mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case e'_2
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
x✝ : { x // x.1 < x.2 }
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist
      (s.points
        (e.symm (↑(if h : e (↑x✝).1 < e (↑x✝).2 then ⟨(e (↑x✝).1, e (↑x✝).2), h⟩ else ⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩)).1))
      (s.points
        (e.symm (↑(if h : e (↑x✝).1 < e (↑x✝).2 then ⟨(e (↑x✝).1, e (↑x✝).2), h⟩ else ⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩)).2))

Tactic:
split

Goal state after:
case e'_2.isTrue
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
x✝ : { x // x.1 < x.2 }
h✝ : e (↑x✝).1 < e (↑x✝).2
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist (s.points (e.symm (↑⟨(e (↑x✝).1, e (↑x✝).2), h✝⟩).1)) (s.points (e.symm (↑⟨(e (↑x✝).1, e (↑x✝).2), h✝⟩).2))

case e'_2.isFalse
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
x✝ : { x // x.1 < x.2 }
h✝ : ¬e (↑x✝).1 < e (↑x✝).2
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist (s.points (e.symm (↑⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩).1)) (s.points (e.symm (↑⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩).2))
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case e'_3
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ (Equiv.swap 0 j) 1 = 1

Tactic:
Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (by lia)

Goal state after:
case e'_3
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) / ↑√π)⁻¹

Tactic:
rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]

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

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖x - (algebraMap ℂ F) z'‖
c : ℂ
n : ℕ
ih : ∀ {p : ℂ[X]}, p.IsMonicOfDegree n → M ^ n ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖
p : ℂ[X]
hp : p.IsMonicOfDegree (n + 1)
⊢ M ^ (n + 1) ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖

Tactic:
obtain ⟨f₁, f₂, hf₁, hf₂, H⟩ := hp.eq_isMonicOfDegree_one_mul_isMonicOfDegree

Goal state after:
case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖x - (algebraMap ℂ F) z'‖
c : ℂ
n : ℕ
ih : ∀ {p : ℂ[X]}, p.IsMonicOfDegree n → M ^ n ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖
p : ℂ[X]
hp : p.IsMonicOfDegree (n + 1)
f₁ f₂ : ℂ[X]
hf₁ : f₁.IsMonicOfDegree 1
hf₂ : f₂.IsMonicOfDegree n
H : p = f₁ * f₂
⊢ M ^ (n + 1) ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
have p : 0 < ‖y‖ := norm_pos_iff.mpr hy
    simpa only [div_add_one hy, norm_div, div_le_iff₀ p, max_mul_of_nonneg _ _ p.le, one_mul,
      div_mul_cancel₀ _ p.ne'] using h (x / y)

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
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this : Tendsto (fun x_1 ↦ ‖(algebraMap ℝ F) x_1.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ sᶜ ×ˢ Set.univ
⊢ ‖(algebraMap ℝ F) w.2‖ - M * ‖x‖ ≤ ‖(algebraMap ℝ F) w.2 - w.1 • x‖

Tactic:
refine le_trans ?_ (norm_sub_norm_le ..)

Goal state after:
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this : Tendsto (fun x_1 ↦ ‖(algebraMap ℝ F) x_1.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ sᶜ ×ˢ Set.univ
⊢ ‖(algebraMap ℝ F) w.2‖ - M * ‖x‖ ≤ ‖(algebraMap ℝ F) w.2‖ - ‖w.1 • x‖
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
⊢ p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))

Tactic:
rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
⊢ p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ (p x ^ s (ψ m)) ^ (1 / ↑(ψ m))
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: case succ
A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n✝ : ℕ
hn : 1 ≤ n✝ + 1
⊢ f (x ^ (n✝ + 1)) = f x ^ (n✝ + 1)

Tactic:
rw [map_pow]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x y : R
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
by
        obtain rfl | hx := eq_or_ne x 0
        · simp
        obtain rfl | hy := eq_or_ne y 0
        · simp
        · simp [hx, hy]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (-x * y) / f y = f (x * y) / f y

Tactic:
rw [neg_mul, f_neg]

Goal state after:
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
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
rw [Metric.tendsto_atTop]

Goal state after:
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
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (smoothingSeminormSeq μ x n) (smoothingFun μ 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 : μ 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
hε2 : 0 < ε / 2
hL2 : ∀ ε_1 > 0, ∃ N, ∀ n ≥ N, dist ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) 1 < ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
⊢ 0 < ε / 2 * (1 / (L + ε / 2))

Tactic:
exact mul_pos hε2
        ((one_div (L + ε / 2)).symm ▸ inv_pos_of_pos (add_pos_of_nonneg_of_pos hL0 hε2))

Goal state after:
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
hε2 : 0 < ε / 2
hL2 : ∀ ε_1 > 0, ∃ N, ∀ n ≥ N, dist ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) 1 < ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
⊢ ∃ m, ∀ n ≥ m, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ δ

Tactic:
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))

Goal state after:
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
hε2 : 0 < ε / 2
hL2 : ∀ ε_1 > 0, ∃ N, ∀ n ≥ N, dist ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) 1 < ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
⊢ ∃ m, ∀ n ≥ m, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ δ
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ BddBelow (Set.range (seminormFromConst_seq c f x))

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ 0 ∈ lowerBounds (Set.range (seminormFromConst_seq c f x))
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
⊢ seminormFromConst_seq c f 0 = 0

Tactic:
seminormFromConst_seq_def

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
⊢ (fun n ↦ f (0 * c ^ n) / f c ^ n) = 0
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), 0 ≤ b → seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (seminormFromConst' c f x * seminormFromConst' c f y))

Tactic:
by
    rw [seminormFromConst_apply_of_isMul hf1 hc hpm hx]
    have hseq : seminormFromConst_seq c f (x * y) =
        fun n ↦ f x * seminormFromConst_seq c f y n := by
      ext n
      simp only [seminormFromConst_seq, mul_assoc, hx, mul_div_assoc]
    simpa [hseq] using (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y).const_mul _

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 : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
this : x ∈ (X - C r).aroots S
⊢ x = (algebraMap R S) r

Tactic:
simpa [aroots_X_sub_C] using this

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
⊢ ‖X.coeff n - (C r).coeff n‖ ^ (1 - ↑n)⁻¹ = ‖r‖

Tactic:
hn,

Goal state after:
case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
⊢ ‖X.coeff 0 - (C r).coeff 0‖ ^ (1 - ↑0)⁻¹ = ‖r‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue p = 0
⊢ p = X ^ p.natDegree

Tactic:
refine hp.eq_X_pow_iff_natDegree_le_natTrailingDegree.mpr <|
    le_natTrailingDegree hp.ne_zero fun n hn ↦ ?_

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue p = 0
n : ℕ
hn : n < p.natDegree
⊢ p.coeff n = 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ mu μ hn n ≤ n

Tactic:
exact mu_le _ _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ BddBelow {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
x : R
ψ : ℕ → ℕ
⊢ 0 ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case pos
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
⊢ ∃ g, f g = 0 ∧ ‖g‖ ≤ (C + ε) * ‖0‖

Tactic:
use 0

Goal state after:
case h
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
⊢ f 0 = 0 ∧ ‖0‖ ≤ (C + ε) * ‖0‖
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
⊢ ∀ (b : ℕ), 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case neg.refine_1
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
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ f g = h

pp: case neg.refine_2
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
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
· -- We indeed get a preimage. First note:
    have : f ∘ s = fun n => ∑ k ∈ range (n + 1), v k := by
      ext n
      simp [s, map_sum, hu]
    /- In the above equality, the left-hand-side converges to `f g` by continuity of `f` and
      definition of `g` while the right-hand-side converges to `h` by construction of `v` so
      `g` is indeed a preimage of `h`. -/
    rw [← this] at lim_v
    exact tendsto_nhds_unique ((f.continuous.tendsto g).comp hg) lim_v

Goal state after:
case neg.refine_2
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
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
⊢ ‖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
⊢ BddBelow {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop, n ≤ a}

Tactic:
use 0

Goal state after:
case h
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
⊢ 0 ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop, n ≤ a}
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

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

Tactic:
rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x✝ : L
k : K
x : L
⊢ (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toFun (k • x) =
    ‖k‖ * (MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f).toFun x

Tactic:
simp only [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe]
        rw [Algebra.smul_def, map_mul]
        congr
        rw [← hf_ext k]
        rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : LeftInverse ⇑finv ⇑f
ginv : G →L[R] F
hginv : LeftInverse ⇑ginv ⇑g
x : E
⊢ finv (ginv (g (f x))) = x

Tactic:
hginv,

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : LeftInverse ⇑finv ⇑f
ginv : G →L[R] F
hginv : LeftInverse ⇑ginv ⇑g
x : E
⊢ finv (f x) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : 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₁
⊢ ∃ t ∈ Filter.map (fun s ↦ ∏ b ∈ s, (fun i ↦ 1 + f i) b) (unconditional ι).filter, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Tactic:
obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)

Goal state after:
ι : 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₁)
⊢ ∃ t ∈ Filter.map (fun s ↦ ∏ b ∈ s, (fun i ↦ 1 + f i) b) (unconditional ι).filter, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
f : ι → R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ ‖∏' (i : ι), (1 + f i)‖ ≠ 0

Tactic:
Multipliable.norm_tprod

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
f : ι → R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ ∏' (i : ι), ‖1 + f i‖ ≠ 0

ι : Type u_1
R : Type u_2
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
f : ι → R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ Multipliable fun i ↦ 1 + f i
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s)
⊢ TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) (fun x ↦ ∏' (i : ι), f i x) atTop s

Tactic:
obtain ⟨r, hr⟩ := hf.exists

Goal state after:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun i x ↦ log (f i x)) r s
⊢ TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) (fun x ↦ ∏' (i : ι), f i x) atTop s