awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
h :
  Eq (α := ℕ → ℝ)
    (fun (n_1 : ℕ) ↦
      if n_1 < n then Norm.norm.{u_1} (E := R) (if n_1 = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑n_1 : ℝ))
      else 0)
    fun (x : ℕ) ↦ 0
⊢ Eq (α := ℝ)
    (⨆ (n_1 : ℕ),
      if n_1 < n then Norm.norm.{u_1} (E := R) (if n_1 = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑n_1 : ℝ))
      else 0)
    0
have convert_4 : Nonempty ℕ
Tactic: convert! ciSup_const using 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
⊢ Eq (α := ℕ → ℝ)
    (fun (n_1 : ℕ) ↦
      if n_1 < n then Norm.norm.{u_1} (E := R) (if n_1 = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑n_1 : ℝ))
      else 0)
    fun (x : ℕ) ↦ 0
have h : ∀ (m : ℕ),
  (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
⊢ (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
have pos : ∀ (hmn : m < n),
  (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
Tactic: by_cases hmn : m < n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
pos :
  ∀ (hmn : m < n),
    (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
      else 0) =
      0
⊢ (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
have neg : ∀ (hmn : ¬m < n),
  (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
Tactic: by_cases hmn : m < n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
hmn : m < n
⊢ (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
have pos : Eq (α := ℝ) 0 0 ∧ ¬n ≤ m
Tactic: rw [if_pos hmn, rpow_eq_zero_iff_of_nonneg (norm_nonneg _), if_neg (_root_.ne_of_lt hmn),
        norm_zero, one_div, ne_eq, inv_eq_zero, ← cast_sub (le_of_lt hmn), cast_eq_zero,
        Nat.sub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
hmn : ¬m < n
⊢ (if m < n then Norm.norm.{u_1} (E := R) (if m = n then 1 else 0) ^ (1 / HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ))
    else 0) =
    0
have neg : Eq (α := ℝ) 0 0
Tactic: rw [if_neg hmn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ spectralValue.{u_1} (R := R) p = 0 ↔ p = HPow.hPow (α := R[X]) X p.natDegree
have refine : ∀ (h : spectralValue.{u_1} (R := R) p = 0), p = HPow.hPow (α := R[X]) X p.natDegree
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ spectralValue_X_pow p.natDegree⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue.{u_1} (R := R) p = 0
⊢ p = HPow.hPow (α := R[X]) X p.natDegree
have refine : ∀ (n : ℕ) (hn : n < p.natDegree), p.coeff n = 0
Tactic: refine hp.eq_X_pow_iff_natDegree_le_natTrailingDegree.mpr <|
    le_natTrailingDegree hp.ne_zero fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue.{u_1} (R := R) p = 0
n : ℕ
hn : n < p.natDegree
⊢ spectralValueTerms.{u_1} (R := R) p n = 0
have apply : 0 ≤ spectralValueTerms.{u_1} (R := R) p n
Tactic: apply le_antisymm ((le_ciSup (spectralValueTerms_bddAbove p) n).trans h.le)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue.{u_1} (R := R) p = 0
n : ℕ
hn : n < p.natDegree
⊢ p.coeff n = 0
have h0 : spectralValueTerms.{u_1} (R := R) p n = 0
Tactic: have h0 : spectralValueTerms p n = 0 := by
    apply le_antisymm ((le_ciSup (spectralValueTerms_bddAbove p) n).trans h.le)
    exact spectralValueTerms_nonneg _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
h : spectralValue.{u_1} (R := R) p = 0
n : ℕ
hn : n < p.natDegree
h0 : spectralValueTerms.{u_1} (R := R) p n = 0
⊢ p.coeff n = 0
have h0₁ : ‖p.coeff n‖ = 0 ∧ 1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) ≠ 0
Tactic: rw [spectralValueTerms_of_lt_natDegree _ hn,
    Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg _)] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
⊢ iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
have refine_1 : ∀ (h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1) (n : ℕ), ‖P.coeff n‖ ≤ 1
Tactic: refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
refine_1 : ∀ (h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1) (n : ℕ), ‖P.coeff n‖ ≤ 1
⊢ iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
have refine_2 : ∀ (h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1), iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
Tactic: refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
⊢ ‖P.coeff n‖ ≤ 1
have refine_1 : ∀ (hPn : P.natDegree < n), ‖P.coeff n‖ ≤ 1
Tactic: obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
refine_1 : ∀ (hPn : P.natDegree < n), ‖P.coeff n‖ ≤ 1
⊢ ‖P.coeff n‖ ≤ 1
have refine_1₁ : ∀ (hPn : P.natDegree = n), ‖P.coeff n‖ ≤ 1
Tactic: obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
refine_1 : ∀ (hPn : P.natDegree < n), ‖P.coeff n‖ ≤ 1
refine_1₁ : ∀ (hPn : P.natDegree = n), ‖P.coeff n‖ ≤ 1
⊢ ‖P.coeff n‖ ≤ 1
have refine_1₂ : ∀ (hPn : n < P.natDegree), ‖P.coeff n‖ ≤ 1
Tactic: obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
hPn : P.natDegree = n
⊢ ‖P.coeff n‖ ≤ 1
have refine_1 : ‖P.coeff P.natDegree‖ ≤ 1
Tactic: rw [← hPn, hP.coeff_natDegree, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
hPn : P.natDegree = n
refine_1 : ‖P.coeff P.natDegree‖ ≤ 1
⊢ ‖P.coeff n‖ ≤ 1
have refine_1₁ : Norm.norm.{u_1} (E := R) 1 ≤ 1
Tactic: rw [← hPn, hP.coeff_natDegree, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
hPn : P.natDegree = n
refine_1 : ‖P.coeff P.natDegree‖ ≤ 1
refine_1₁ : Norm.norm.{u_1} (E := R) 1 ≤ 1
⊢ ‖P.coeff n‖ ≤ 1
have refine_1₂ : LE.le (α := ℝ) 1 1
Tactic: rw [← hPn, hP.coeff_natDegree, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
hPn : n < P.natDegree
⊢ ‖P.coeff n‖ ≤ 1
have this : spectralValueTerms.{u_1} (R := R) P n ≤ 1
Tactic: have : spectralValueTerms P n ≤ 1 := le_ciSup (spectralValueTerms_bddAbove P) n |>.trans h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
hPn : n < P.natDegree
this : spectralValueTerms.{u_1} (R := R) P n ≤ 1
⊢ ‖P.coeff n‖ ≤ 1
have refine_1 : ∀ (this : 1 < ‖P.coeff n‖), 1 < spectralValueTerms.{u_1} (R := R) P n
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
n : ℕ
hPn : n < P.natDegree
this : 1 < ‖P.coeff n‖
⊢ 1 < spectralValueTerms.{u_1} (R := R) P n
have refine_1 : 1 < ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ))
Tactic: simp only [spectralValueTerms_of_lt_natDegree _ hPn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
⊢ iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
have apply : ∀ (n : ℕ), spectralValueTerms.{u_1} (R := R) P n ≤ 1
Tactic: apply ciSup_le (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
⊢ (if n < P.natDegree then ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) else 0) ≤ 1
have pos : ∀ (hn : n < P.natDegree), ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) ≤ 1
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
pos : ∀ (hn : n < P.natDegree), ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) ≤ 1
⊢ (if n < P.natDegree then ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) else 0) ≤ 1
have neg : ∀ (hn : ¬n < P.natDegree), LE.le (α := ℝ) 0 1
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : n < P.natDegree
⊢ ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) ≤ 1
have pos : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)
Tactic: apply Real.rpow_le_one (norm_nonneg _) (h n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : n < P.natDegree
⊢ 0 ≤ 1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)
have pos : n ≤ P.natDegree
Tactic: rw [one_div_nonneg, sub_nonneg, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
⊢ (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
have pos : ∀ (hx0 : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)), (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
Tactic: by_cases hx0 : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
pos : ∀ (hx0 : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)), (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
⊢ (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
have neg : ∀ (hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)), (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
Tactic: by_cases hx0 : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
⊢ (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
have pos : 0 ≤ spectralValue.{u_2} (R := K) p
Tactic: rw [hx0]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
⊢ (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
have neg : ∀ (h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p), False
Tactic: by_contra h_ge
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw : HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
  ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
    ‖p.coeff n‖
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw₁ : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) * (↑(p.natDegree - n) : ℝ)) = ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
    ‖p.coeff n‖
rw₁ : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) * (↑(p.natDegree - n) : ℝ)) = ‖p.coeff n‖
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw₂ : ‖p.coeff n‖ ^ ((↑(p.natDegree - n) : ℝ) * (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) = ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
    ‖p.coeff n‖
rw₁ : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) * (↑(p.natDegree - n) : ℝ)) = ‖p.coeff n‖
rw₂ : ‖p.coeff n‖ ^ ((↑(p.natDegree - n) : ℝ) * (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) = ‖p.coeff n‖
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw₃ : HPow.hPow (β := ℝ) ‖p.coeff n‖ (↑(p.natDegree - n) : ℝ) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) =
  ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
    ‖p.coeff n‖
rw₁ : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) * (↑(p.natDegree - n) : ℝ)) = ‖p.coeff n‖
rw₂ : ‖p.coeff n‖ ^ ((↑(p.natDegree - n) : ℝ) * (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) = ‖p.coeff n‖
rw₃ :
  HPow.hPow (β := ℝ) ‖p.coeff n‖ (↑(p.natDegree - n) : ℝ) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) =
    ‖p.coeff n‖
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw₄ : (‖p.coeff n‖ ^ (p.natDegree - n)) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) = ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
    ‖p.coeff n‖
rw₁ : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) * (↑(p.natDegree - n) : ℝ)) = ‖p.coeff n‖
rw₂ : ‖p.coeff n‖ ^ ((↑(p.natDegree - n) : ℝ) * (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) = ‖p.coeff n‖
rw₃ :
  HPow.hPow (β := ℝ) ‖p.coeff n‖ (↑(p.natDegree - n) : ℝ) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) =
    ‖p.coeff n‖
rw₄ : (‖p.coeff n‖ ^ (p.natDegree - n)) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) = ‖p.coeff n‖
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw₅ : (‖p.coeff n‖ ^ (p.natDegree - n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(p.natDegree - n) : ℝ) = ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
p : K[X]
hp : p.Monic
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
hx0 : ¬Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
n : ℕ
hn : n < p.natDegree
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) =
    ‖p.coeff n‖
rw₁ : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) * (↑(p.natDegree - n) : ℝ)) = ‖p.coeff n‖
rw₂ : ‖p.coeff n‖ ^ ((↑(p.natDegree - n) : ℝ) * (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) = ‖p.coeff n‖
rw₃ :
  HPow.hPow (β := ℝ) ‖p.coeff n‖ (↑(p.natDegree - n) : ℝ) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) =
    ‖p.coeff n‖
rw₄ : (‖p.coeff n‖ ^ (p.natDegree - n)) ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) = ‖p.coeff n‖
rw₅ : (‖p.coeff n‖ ^ (p.natDegree - n)) ^ HDiv.hDiv (α := ℝ) 1 (↑(p.natDegree - n) : ℝ) = ‖p.coeff n‖
⊢ (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
have rw₆ : HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (p.natDegree - n)) (↑(p.natDegree - n) : ℝ)⁻¹ = ‖p.coeff n‖
Tactic: rw [← rpow_natCast, ← rpow_mul (norm_nonneg _), mul_comm, rpow_mul (norm_nonneg _),
          rpow_natCast, ← cast_sub (le_of_lt hn), one_div,
          pow_rpow_inv_natCast (norm_nonneg _) (_root_.ne_of_gt (tsub_pos_of_lt hn))]