mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹² : Field k
inst✝¹¹ : LinearOrder k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : AddTorsor V P
inst✝⁷ : TopologicalSpace V
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
h : s ∈ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)
⊢ s ∈ (map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)).bind 𝓝

Tactic:
← nhds_bind_nhds

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹² : Field k
inst✝¹¹ : LinearOrder k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : AddTorsor V P
inst✝⁷ : TopologicalSpace V
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
h : s ∈ map (fun x ↦ x +ᵥ p) (atTop • (𝓝 v).bind 𝓝)
⊢ s ∈ (map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)).bind 𝓝
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
i : ↑s
r : k
hr :
  (Finset.affineCombination k (fs i) p) ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
hind :
  (↑(fs i)).indicator ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (↑(fs ⟨i', hi'⟩)).indicator ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
j : ι
hj : j = ↑i
⊢ r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j

Tactic:
simp [hj]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case zero
s : ℂ
⊢ ⌊1 - s.re⌋₊ = 0 → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
intro hs

Goal state after:
case zero
s : ℂ
hs : ⌊1 - s.re⌋₊ = 0
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
⊢ ⌊1 - s.re⌋₊ = m + 1 → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
intro hs

Goal state after:
case succ
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
by rw [le_add_iff_nonneg_right]; apply norm_nonneg

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n ↦ 1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))

Tactic:
· have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by simp
    convert! tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)
    rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne]
    convert! tendsto_euler_sin_prod z using 1
    ext1 n; rw [mul_comm, ← mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n - 2)
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
rw [show 2 * n - 2 = 2 * (n - 1) by grind] at hp

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
⊢ ∃ m, ∀ n ≥ m, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))

Tactic:
by
    have hε2 : 0 < ε / 2 := half_pos hε
    have hL2 := smoothingSeminormSeq_tendsto_aux μ hL0 hε2 (PNat.pos m1) hx
    rw [Metric.tendsto_atTop] at hL2
    set δ : ℝ := ε / (2 * (L + ε / 2)) with hδ_def
    have hδ : 0 < δ := by
      rw [hδ_def, div_mul_eq_div_mul_one_div]
      exact mul_pos hε2
        ((one_div (L + ε / 2)).symm ▸ inv_pos_of_pos (add_pos_of_nonneg_of_pos hL0 hε2))
    obtain ⟨N, hN⟩ := hL2 δ hδ
    use N
    intro n hn
    specialize hN n hn
    rw [Real.dist_eq, abs_lt] at hN
    exact le_of_lt hN.right

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
r : R
x : S
h : IsConjRoot R ((algebraMap R S) r) x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x = (algebraMap R S) r

Tactic:
by
  rw [IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj _ hf] at h
  have : x ∈ (X - C r).aroots S := by
    rw [mem_aroots]
    simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]
  simpa [aroots_X_sub_C] using this

Goal state after:
Module: Mathlib.Analysis.Normed.Group.CocompactMap

Goal state before:
pp: E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖

Tactic:
have h := cocompact_tendsto f
  rw [tendsto_def] at h
  specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)
  rcases closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
  use r
  intro x hx
  suffices x ∈ f ⁻¹' (Metric.closedBall 0 ε)ᶜ by simp_all
  apply hr
  simp [hx]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ a' ∈ (minpoly L a).rootSet F ∧ a' ≠ a

Tactic:
rw [← (isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩)]

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ IsConjRoot L a a' ∧ a' ≠ a
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
have hψ : ∀ n, 0 ≤ 1 / (ψ n : ℝ) := fun _ ↦ by simp only [one_div, inv_nonneg, cast_nonneg]
  by_cases! hx : μ x ≤ 1
  · use 1
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    exact rpow_le_one (apply_nonneg _ _) hx (div_nonneg (cast_nonneg _) (cast_nonneg _))
  · use μ x
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    conv_rhs => rw [← rpow_one (μ x)]
    rw [rpow_le_rpow_left_iff hx]
    exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (cast_nonneg _)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case neg
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
obtain
    ⟨v : ℕ → H, lim_v : Tendsto (fun n : ℕ => ∑ k ∈ range (n + 1), v k) atTop (𝓝 h), v_in :
      ∀ n, v n ∈ K, hv₀ : ‖-v 0 + h‖ < b 0, hv : ∀ n > 0, ‖v n‖ < b n⟩ :=
    controlled_sum_of_mem_closure h_in b_pos

Goal state after:
case neg
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ 1 = smoothingFun μ x ^ a

Tactic:
ha,

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ 1 = smoothingFun μ x ^ 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
have ha_pos : 0 < a := lt_of_le_of_ne a_in.1 (Ne.symm ha)

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X✝ Y✝ : SemiNormedGrp₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : Y✝.carrier
⊢ ↑(Hom.hom ((cokernelCocone f).π ≫ cokernelLift f s)) x✝ = ↑(Hom.hom (Cofork.π s)) x✝

Tactic:
apply NormedAddGroupHom.lift_mk f.1.range

Goal state after:
X✝ Y✝ : SemiNormedGrp₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : Y✝.carrier
⊢ ∀ s_1 ∈ f.hom'.range, (Cofork.π s).hom' s_1 = 0
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
⊢ 0 ≫ h = 0

Tactic:
Limits.zero_comp

Goal state after:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
⊢ 0 = 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
h1 : μ 1 = 1
hn0 : ↑n ≠ 0
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Tactic:
← mul_one (x ^ n),

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
h1 : μ 1 = 1
hn0 : ↑n ≠ 0
⊢ μ (x ^ n * 1) ^ (1 / ↑n) = μ x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
⊢ smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y

Tactic:
have hlim : Tendsto (fun n => μ x * smoothingSeminormSeq μ y n) atTop
      (𝓝 (smoothingFun μ x * smoothingFun μ y)) := by
    rw [smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx]
    exact Tendsto.const_mul _ (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y)

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
⊢ smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ∏ x ∈ b, (1 + f x) ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)

Tactic:
← union_sdiff_of_subset hb,

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ∏ x ∈ s ∪ b \ s, (1 + f x) ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q : ℝ≥0∞
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e ∞
hf : Memℓp f q
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) q

Tactic:
by
  obtain (h | h) := isEmpty_or_nonempty ι
  · exact all _
  obtain ⟨C, hC⟩ := by
    simpa [memℓp_infty_iff, BddAbove, Set.Nonempty, Set.range, upperBounds] using he
  refine hf.norm.const_mul (K * C) |>.mono fun i ↦ ?_
  have hK_nonneg : 0 ≤ K := norm_nonneg (B (Classical.arbitrary ι)) |>.trans <| hBK _
  calc
    ‖B i (e i) (f i)‖ ≤ ‖B i‖ * ‖e i‖ * ‖f i‖ := (B i (e i)).le_of_opNorm_le ((B i).le_opNorm _) _
    _ ≤ K * C * ‖f i‖ := by gcongr; exacts [hBK i, hC i]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w✝¹ : SeminormedAddCommGroup G
w✝ : NormedSpace 𝕜 G
h : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
x : ⨂[𝕜] (i : ι), E i
⊢ ((normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)) x ≤
    projectiveSeminorm x

Tactic:
simp only [Seminorm.comp_apply, coe_normSeminorm]

Goal state after:
case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w✝¹ : SeminormedAddCommGroup G
w✝ : NormedSpace 𝕜 G
h : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(toDualContinuousMultilinearMap G) x‖ ≤ projectiveSeminorm x
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
⊢ ∃ x, ¬v x = 0

Tactic:
exact ⟨u, huv⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝¹ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this✝ : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
this : 0 ≤ α • 1
⊢ 0 ≤ α

Tactic:
← LinearMap.isPositive_one.isPositive_smul_iff (E := V) (one_ne_zero' (V →ₗ[𝕜] V))

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝¹ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this✝ : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
this : 0 ≤ α • 1
⊢ (α • 1).IsPositive
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ s = {t | t * a⁻¹ ∈ a⁻¹ • s}

Tactic:
· ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

Goal state after:
case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ s = {t | t * a⁻¹ ∈ a⁻¹ • s}
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a)
⊢ t₀ = t₀ / a / a⁻¹

Tactic:
· ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

Goal state after:
case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (t₀ / a)
⊢ t₀ = t₀ / a / a⁻¹
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a)
⊢ v = a⁻¹ • (a • v ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

Tactic:
· ext t
    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ |↑K| ^ (n + 1) * (|(|↑t - ↑t₀|)| ^ (n + 1) / |↑n + 1|) / |↑n !| * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
NNReal.abs_eq,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ↑K ^ (n + 1) * (|(|↑t - ↑t₀|)| ^ (n + 1) / |↑n + 1|) / |↑n !| * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β