awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)

Tactic:
have h_rg : ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) ∈
          Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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‖
h_rg :
  ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) ∈ Set.range (spectralValueTerms.{u_2} (R := K) p)
⊢ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x

Tactic:
h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg

Premises used: NNNorm.nnnorm, HSub.hSub, HDiv.hDiv, Nat.cast, Polynomial.coeff, HPow.hPow, Polynomial.natDegree, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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‖
h_rg :
  ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) ∈ Set.range (spectralValueTerms.{u_2} (R := K) p)
⊢ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) < (f : (a : L) → ℝ) x

Tactic:
exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg

Premises used: NNNorm.nnnorm, HSub.hSub, HDiv.hDiv, Nat.cast, Polynomial.coeff, HPow.hPow, Polynomial.natDegree, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

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
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
rw :
  HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) <
    HPow.hPow (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) x : ℝ) (↑(p.natDegree - n) : ℝ)
⊢ ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)

Tactic:
rw [← hexp, ← rpow_natCast, ← rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
hz : LT.lt (α := ℝ) 0 (↑(p.natDegree - n) : ℝ)
⊢ HPow.hPow (β := ℝ) (‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))) (↑(p.natDegree - n) : ℝ) <
    HPow.hPow (α := ℝ) (β := ℝ) ((f : (a : L) → ℝ) x : ℝ) (↑(p.natDegree - n) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ LT.lt (α := ℝ) 0 (↑(p.natDegree - n) : ℝ)

Tactic:
cast_pos.mpr (tsub_pos_of_lt hn)

Premises used: Iff.mpr, Nat.cast_pos, tsub_pos_of_lt
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ LT.lt (α := ℝ) 0 (↑(p.natDegree - n) : ℝ)

Tactic:
exact cast_pos.mpr (tsub_pos_of_lt hn)

Premises used: Iff.mpr, Nat.cast_pos, tsub_pos_of_lt
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)

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)
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)
⊢ 0 < p.natDegree

Tactic:
have h_deg : 0 < p.natDegree := natDegree_pos_of_monic_of_aeval_eq_zero hp hx
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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) : ℝ)
neg :
  ∀ (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) : ℝ)

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
pos :
  HMul.hMul (β := ℝ) ‖p.coeff n‖ ((f : (a : L) → ℝ) 1 : ℝ) <
    HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg),
            ← Nat.sub_zero p.natDegree, ← hn0]

Premises used: Iff.mpr, pow_zero, SeminormClass.map_smul_eq_mul, Nat.sub_zero, Polynomial.natDegree, Nat.succ_le_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ HMul.hMul (β := ℝ) ‖p.coeff n‖ ((f : (a : L) → ℝ) 1 : ℝ) <
    HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)

Tactic:
(mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)

Premises used: IsPowMul.map_one_le_one, mul_le_of_le_one_right, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ HMul.hMul (β := ℝ) ‖p.coeff n‖ ((f : (a : L) → ℝ) 1 : ℝ) <
    HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)

Tactic:
exact (mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)

Premises used: IsPowMul.map_one_le_one, mul_le_of_le_one_right, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
rw rw₁ : p.natDegree = p.natDegree
⊢ p.natDegree = p.natDegree - n + n

Tactic:
rw [Nat.sub_add_cancel (le_of_lt hn)]

Premises used: le_of_lt, Nat.sub_add_cancel
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

Tactic:
have : p.natDegree = p.natDegree - n + n := by rw [Nat.sub_add_cancel (le_of_lt hn)]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
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
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (p.coeff n • x ^ n) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

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]

Premises used: Iff.mpr, pow_add, SeminormClass.map_smul_eq_mul, Iff.mp, Nat.succ_le_iff, pos_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
neg : ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - 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

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ) (p.natDegree - n)

Tactic:
hn_lt n hn
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ) (p.natDegree - n)

Tactic:
exact hn_lt n hn
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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) : ℝ)

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
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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) : ℝ)
set :
  let g : (i : ℕ) → L := fun (i : ℕ) ↦ p.coeff i • x ^ i;
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
set g := fun i : ℕ ↦ p.coeff i • x ^ i

Premises used: Polynomial.coeff, HPow.hPow, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
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) : ℝ)
⊢ ∃ (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)

Premises used: IsNonarchimedean.finset_image_add, Finset.range, Polynomial.natDegree