mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun n ↦ (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!) c
hs : HasSum (fun n ↦ (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s
⊢ HasSum (fun n ↦ (expSeries ℝ ℍ n) fun x ↦ q) (↑c + (s / ‖q‖) • q)

Tactic:
replace hc := hasSum_coe.mpr hc

Goal state after:
q : ℍ
hq : q.re = 0
c s : ℝ
hs : HasSum (fun n ↦ (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
⊢ HasSum (fun n ↦ (expSeries ℝ ℍ n) fun x ↦ q) (↑c + (s / ‖q‖) • q)
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ (if x * y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) * if y = 0 then 0 else 1

Tactic:
simp only [if_false, h, left_ne_zero_of_mul h, right_ne_zero_of_mul h, mul_one,
            le_refl]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
· specialize f_mul x 1
    rw [mul_one, h1, mul_zero] at f_mul
    have hx0 : f x = 0 := f_mul.antisymm (f_nonneg _)
    rw [hx0, h1, zero_mul]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ seminormFromBounded' f x = f x

Tactic:
simp_rw [seminormFromBounded', hx, ← mul_div_assoc']

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ ⨆ y, f x * (f y / f y) = f x
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
⊢ ∃ c, ∃ (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y

Tactic:
obtain ⟨c, _, hc⟩ := exists_mem_eq_sup' univ_nonempty (fun i : ι × ι ↦ B.norm (B i.1 * B i.2))
  use B.norm (B c.1 * B c.2)
  constructor
  -- ∀ (x y : L), B.norm (x * y) ≤ B.norm (⇑B c.fst * ⇑B c.snd) * B.norm x * B.norm y
  · intro x y
    -- `ixy` is an index for which `‖B.repr (x*y) i‖` is maximum.
    obtain ⟨ixy, _, hixy_def⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖(B.repr (x * y)) i‖)
    -- We rewrite the LHS using `ixy`.
    conv_lhs => simp only [Basis.norm]; rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]
    rw [sum_mul, map_finsetSum]
    simp_rw [smul_mul_assoc, map_smul, mul_sum, map_finsetSum, mul_smul_comm, map_smul]
    have hna' : IsNonarchimedean (NormedField.toMulRingNorm K) := hna
    /- Since the norm is nonarchimedean, the norm of a finite sum is bounded by the maximum of the
          norms of the summands. -/
    obtain ⟨k, -, (hk : ‖∑ i : ι, (B.repr x i • ∑ i_1 : ι,
      B.repr y i_1 • B.repr (B i * B i_1)) ixy‖ ≤
      ‖(B.repr x k • ∑ j : ι, B.repr y j • B.repr (B k * B j)) ixy‖)⟩ :=
      IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hna'
        (fun i ↦ (B.repr x i • ∑ i_1 : ι, B.repr y i_1 • B.repr (B i * B i_1)) ixy)
        (univ : Finset ι)
    simp only [Finsupp.coe_smul, Finsupp.coe_finsetSum, Pi.smul_apply, Finset.sum_apply,
      smul_eq_mul, norm_mul] at hk ⊢
    apply le_trans hk
    -- We use the above property again.
    obtain ⟨k', hk'⟩ : ∃ (k' : ι),
        ‖∑ j : ι, B.repr y j • B.repr (B k * B j) ixy‖ ≤
          ‖B.repr y k' • B.repr (B k * B k') ixy‖ := by
      obtain ⟨k, hk0, hk⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hna'
        (fun i ↦ B.repr y i • B.repr (B k * B i) ixy) (univ : Finset ι)
      exact ⟨k, hk⟩
    apply le_trans (mul_le_mul_of_nonneg_left hk' (norm_nonneg _))
    -- Now an easy computation leads to the desired conclusion.
    rw [norm_smul, mul_assoc, mul_comm (B.norm (B c.fst * B c.snd)), ← mul_assoc]
    exact mul_le_mul (mul_le_mul (B.norm_repr_le_norm _) (B.norm_repr_le_norm _)
      (norm_nonneg _) (B.norm_nonneg _)) (le_trans (B.norm_repr_le_norm _)
        (hc ▸ Finset.le_sup' (fun i : ι × ι ↦ B.norm (B i.1 * B i.2)) (mem_univ (k, k'))))
      (norm_nonneg _) (mul_nonneg (B.norm_nonneg _) (B.norm_nonneg _))
    -- `B c.1 * B c.2` is positive.
  · have h_pos : (0 : ℝ) < B.norm (B i * B i) := by
      have h1 : (1 : L) = (algebraMap K L) 1 := by rw [map_one]
      rw [hBi, mul_one, h1, Basis.norm_extends hBi]
      simp [norm_one, zero_lt_one]
    exact lt_of_lt_of_le h_pos
      (hc ▸ Finset.le_sup' (fun i : ι × ι ↦ B.norm (B i.1 * B i.2)) (mem_univ (i, i)))

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
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))

Tactic:
have hm10 : (m1 : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (PNat.pos m1))

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
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
hm10 : ↑↑m1 ≠ 0
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
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
n : ℕ
⊢ f (c ^ n * c) / f c ^ n = f c

Tactic:
← pow_succ,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
n : ℕ
⊢ f (c ^ (n + 1)) / f c ^ n = f c
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
⊢ ∀ (u : ℕ → E), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
intro u

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
⊢ CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : f x = 0
⊢ f x ≤ spectralValue p

pp: case neg
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
⊢ f x ≤ spectralValue p

Tactic:
· rw [hx0]; exact spectralValue_nonneg p

Goal state after:
case neg
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
⊢ f x ≤ spectralValue p
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: 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'
⊢ δ ≤ ‖a - a'‖

Tactic:
by_cases hS : S.Nonempty

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
⊢ δ ≤ ‖a - a'‖

case neg
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 - a'‖
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: 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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
⊢ δ > 0

Tactic:
by_cases hS : S.Nonempty

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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ δ > 0

case neg
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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ δ > 0
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
n : ℕ
hn : 1 ≤ n
⊢ μ 1 ^ (1 / ↑n) ≤ 1 ^ (1 / ↑n)

Tactic:
have hn1 : 0 < (1 / n : ℝ) := by
    apply _root_.div_pos zero_lt_one
    rw [← cast_zero, cast_lt]
    exact succ_le_iff.mp hn

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
hn1 : 0 < 1 / ↑n
⊢ μ 1 ^ (1 / ↑n) ≤ 1 ^ (1 / ↑n)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
hn' : ∀ n < p.natDegree, f (p.coeff n • x ^ n) < f (x ^ p.natDegree)
g : ℕ → L := fun i ↦ p.coeff i • x ^ i
m : ℕ
hm : 0 < p.natDegree → m < p.natDegree
h : f ((Finset.range p.natDegree).sum g) ≤ f (g m)
⊢ ∃ m, ∃ (_ : 0 < p.natDegree → m < p.natDegree), f ((Finset.range p.natDegree).sum g) ≤ f (g m)

Tactic:
exact ⟨m, hm, h⟩

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt : f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) < f (x ^ p.natDegree)
⊢ f (1 • x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) = f (x ^ p.natDegree)

Tactic:
one_smul,

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt : f (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) < f (x ^ p.natDegree)
⊢ f (x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) = f (x ^ p.natDegree)
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
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
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ (x ^ s (ψ b)) ^ (1 / ↑(ψ b)) ≤ x_1) → 0 ≤ x_1

Tactic:
exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊
hf_iso : ∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)
x : L
σ : Gal(L/K)
⊢ f (σ x) = f x

Tactic:
hf_iso σ x

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊
hf_iso : ∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)
x : L
σ : Gal(L/K)
⊢ f (σ x) = f (σ x)
Module: Mathlib.Analysis.Normed.Lp.LpEquiv

Goal state before:
pp: case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ∞)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
PiLp.norm_eq_ciSup,

Goal state after:
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ∞)
⊢ ⨆ i, ‖(Equiv.lpPiLp f).ofLp i‖ = ‖f‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case neg
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
x y : L
hx : ¬x = 0
hx' : (spectralAlgNorm K L) x ≠ 0
hf1 : (spectralAlgNorm K L) 1 ≤ 1
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
hf_pow : IsPowMul ⇑f
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

Tactic:
← spectralNorm_unique hf_pow,

Goal state after:
case neg
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
x y : L
hx : ¬x = 0
hx' : (spectralAlgNorm K L) x ≠ 0
hf1 : (spectralAlgNorm K L) 1 ≤ 1
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
hf_pow : IsPowMul ⇑f
⊢ f (x * y) = f x * f y
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed ↑(↑f).range

Tactic:
f.range_eq_ker_of_leftInverse (hf.leftInverse_leftInverse)

Goal state after:
R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed ↑(↑f ∘ₗ ↑hf.leftInverse - LinearMap.id).ker
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (1 • R • x - P • R • x)‖ + ‖(1 - R) • (1 • R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 • R • x - P • R • x)‖)

Tactic:
one_smul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (R • x - P • R • x)‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • (1 • R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)

Tactic:
one_smul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ Commute P Q

Tactic:
by
  have PR_eq_RPR : ∀ R : M, IsLprojection X R → P * R = R * P * R := fun R h₃ => by
    refine @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
      rw [← norm_sub_eq_zero_iff]
      have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
        calc
          ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) := by
            rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
          _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) := by
            rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
          _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
              (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
            rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
          _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
          _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ := by
            rw [ge_iff_le]
            have :=
              add_le_add_left (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
            simpa only [mul_smul, sub_smul, one_smul] using this
      rw [two_smul] at e1
      nlinarith [e1, norm_nonneg ((P * R) • x - (R * P * R) • x)]
  have QP_eq_QPQ : Q * P = Q * P * Q := by
    have e1 : Q * P - Q * P * Q = 0 := by
      calc
        Q * P - Q * P * Q = P * (1 - Q) - (1 - Q) * P * (1 - Q) := by noncomm_ring
        _ = 0 := sub_eq_zero.mpr (PR_eq_RPR (1 - Q) h₂.Lcomplement)
    simpa [sub_eq_zero] using e1
  change P * Q = Q * P
  rw [QP_eq_QPQ, PR_eq_RPR Q h₂]

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖1 • Q • x - P • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)

Tactic:
one_smul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)