awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
rw₆ : HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (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.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 (hypothesis)
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‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
have hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
Tactic: have hexp : (‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ))) ^ (p.natDegree - n) =
          ‖p.coeff n‖ := by
        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
hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x
have rw : ∀ (h_ge : ∀ x_1 ∈ Set.range (spectralValueTerms.{u_2} (R := K) p), x_1 < (f : (a : L) → ℝ) x) (n : ℕ)
  (hn : n < p.natDegree)
  (hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖),
  ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x
Tactic: rw [spectralValue, iSup, not_le, Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
          (Set.range_nonempty (spectralValueTerms p))] at h_ge
Cleared hypotheses: h_ge, n, hn, hexp
-- 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 : ∀ x_1 ∈ Set.range (spectralValueTerms.{u_2} (R := K) p), x_1 < (f : (a : L) → ℝ) x
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) ∈ Set.range (spectralValueTerms.{u_2} (R := K) p)
have h : spectralValueTerms.{u_2} (R := K) p n = ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))
Tactic: use n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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 : ∀ x_1 ∈ Set.range (spectralValueTerms.{u_2} (R := K) p), x_1 < (f : (a : L) → ℝ) x
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x
have h_rg : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) ∈ Set.range (spectralValueTerms.{u_2} (R := K) p)
Tactic: have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈
          Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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
hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
⊢ ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
have h_base : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x
Tactic: have h_base : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) < f x := by
        rw [spectralValue, iSup, not_le, Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
          (Set.range_nonempty (spectralValueTerms p))] at h_ge
        have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈
          Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
        exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg
-- 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
hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
h_base : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x
⊢ ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
have rw : HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) <
  HPow.hPow (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) x : ℝ) (↑(p.natDegree - n) : ℝ)
Tactic: rw [← hexp, ← rpow_natCast, ← rpow_natCast]
-- 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
hexp : (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) ^ (p.natDegree - n) = ‖p.coeff n‖
h_base : ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x
⊢ HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) <
    HPow.hPow (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) x : ℝ) (↑(p.natDegree - n) : ℝ)
have hz : LT.lt (α := ℝ) 0 (↑(p.natDegree - n) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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
⊢ False
have hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
Tactic: have hn_lt (n : ℕ) (hn : n < p.natDegree) : ‖p.coeff n‖ < f x ^ (p.natDegree - n) := by
      have hexp : (‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ))) ^ (p.natDegree - n) =
          ‖p.coeff n‖ := by
        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))]
      have h_base : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) < f x := by
        rw [spectralValue, iSup, not_le, Set.Finite.csSup_lt_iff (spectralValueTerms_finite_range p)
          (Set.range_nonempty (spectralValueTerms p))] at h_ge
        have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈
          Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
        exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg
      rw [← hexp, ← rpow_natCast, ← rpow_natCast]
      gcongr
      exact cast_pos.mpr (tsub_pos_of_lt hn)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
⊢ False
have h_deg : 0 < p.natDegree
Tactic: have h_deg : 0 < p.natDegree := natDegree_pos_of_monic_of_aeval_eq_zero hp hx
-- 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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have pos : ∀ (hn0 : n = 0), LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
Tactic: by_cases hn0 : n = 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 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
pos :
  ∀ (hn0 : n = 0), LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have neg : ∀ (hn0 : ¬n = 0), LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
Tactic: by_cases hn0 : n = 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 : ℝ)
h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : n = 0
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have pos : HMul.hMul (β := ℝ) ‖p.coeff n‖ ((f : (a : L) → ℝ) 1 : ℝ) <
  HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
Tactic: rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg),
            ← Nat.sub_zero p.natDegree, ← hn0]
-- 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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
⊢ p.natDegree = p.natDegree - n + n
have rw : p.natDegree = p.natDegree
Tactic: rw [Nat.sub_add_cancel (le_of_lt hn)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have this : p.natDegree = p.natDegree - n + n
Tactic: have : p.natDegree = p.natDegree - n + n := by rw [Nat.sub_add_cancel (le_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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
this : p.natDegree = p.natDegree - n + n
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have neg : ‖p.coeff n‖ * HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) n <
  HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n) * HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) n
Tactic: rw [map_smul_eq_mul, hf_pm _ (succ_le_iff.mp (pos_iff_ne_zero.mpr hn0)),
            hf_pm _ (succ_le_iff.mpr h_deg), this, pow_add]
-- 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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
this : p.natDegree = p.natDegree - n + n
⊢ ‖p.coeff n‖ * HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) n <
    HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n) * HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) n
have neg : ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have hn' : ∀ (n : ℕ) (hn : n < p.natDegree),
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
Tactic: have hn' (n : ℕ) (hn : n < p.natDegree) : f (p.coeff n • x ^ n) < f (x ^ p.natDegree) := by
        by_cases hn0 : n = 0
        · rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg),
            ← Nat.sub_zero p.natDegree, ← hn0]
          exact (mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)
        · have : p.natDegree = p.natDegree - n + n := by rw [Nat.sub_add_cancel (le_of_lt hn)]
          rw [map_smul_eq_mul, hf_pm _ (succ_le_iff.mp (pos_iff_ne_zero.mpr hn0)),
            hf_pm _ (succ_le_iff.mpr h_deg), this, pow_add]
          gcongr
          exact hn_lt n 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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
hn' :
  ∀ (n : ℕ) (hn : n < p.natDegree),
    LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
g : (i : ℕ) → L := fun (i : ℕ) ↦ p.coeff i • x ^ i
⊢ ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
    LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)
have obtain : ∀ (m : ℕ) (hm : (Finset.range p.natDegree).Nonempty → m ∈ Finset.range p.natDegree)
  (h : LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)),
  ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
    LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)
Tactic: obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add hf_na g (Finset.range p.natDegree)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
hn' :
  ∀ (n : ℕ) (hn : n < p.natDegree),
    LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
g : (i : ℕ) → L := fun (i : ℕ) ↦ p.coeff i • x ^ i
m : ℕ
hm : (Finset.range p.natDegree).Nonempty → m ∈ Finset.range p.natDegree
h : LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)
⊢ ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
    LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)
have hm₁ : 0 < p.natDegree → m < p.natDegree
Tactic: rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
Cleared hypotheses: hm, h