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 : ¬(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) : ℝ)
⊢ 0 < p.natDegree → m < p.natDegree

Tactic:
rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm

Premises used: Finset.nonempty_range_iff, Finset.mem_range, zero_lt_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
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) : ℝ)
hm₁ : 0 < p.natDegree → m < p.natDegree
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)

Tactic:
rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm

Premises used: Finset.nonempty_range_iff, Finset.mem_range, zero_lt_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
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 : 0 < p.natDegree → m < 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:
⟨m, hm, h⟩

Premises used: Exists.intro
-- 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
m : ℕ
hm : 0 < p.natDegree → m < 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:
exact ⟨m, hm, h⟩
-- 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_in : 0 < p.natDegree → m < p.natDegree)
    (hm : LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)),
    LT.lt (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
obtain ⟨m, hm_in, hm⟩ : ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
          f ((Finset.range p.natDegree).sum g) ≤ f (g m) := by
        obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add hf_na g (Finset.range p.natDegree)
        rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
        exact ⟨m, hm, h⟩

Premises used: Finset.range, Polynomial.natDegree, DFunLike.coe, Finset.sum
-- 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
m : ℕ
hm_in : 0 < p.natDegree → m < p.natDegree
hm : LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
lt_of_le_of_lt hm (hn' m (hm_in h_deg))

Premises used: lt_of_le_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
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_in : 0 < p.natDegree → m < p.natDegree
hm : LE.le (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (g m) : ℝ)
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
exact lt_of_le_of_lt hm (hn' m (hm_in h_deg))

Premises used: lt_of_le_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
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) : ℝ)

Tactic:
have h_lt : f ((Finset.range p.natDegree).sum fun i : ℕ ↦ p.coeff i • x ^ i) <
        f (x ^ p.natDegree) := by
      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
      set g := fun i : ℕ ↦ p.coeff i • x ^ i
      obtain ⟨m, hm_in, hm⟩ : ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
          f ((Finset.range p.natDegree).sum g) ≤ f (g m) := by
        obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add hf_na g (Finset.range p.natDegree)
        rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
        exact ⟨m, hm, h⟩
      exact lt_of_le_of_lt hm (hn' m (hm_in h_deg))
-- 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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
rw :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) : ℝ)
    (max ((f : (a : L) → ℝ) (x ^ p.natDegree)) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i)) :
      ℝ)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree,
          one_smul, ← max_eq_left_of_lt h_lt]

Premises used: add_comm, one_smul, Polynomial.aeval_eq_sum_range, Polynomial.Monic.coeff_natDegree, max_eq_left_of_lt, Finset.sum_range_succ
-- 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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) : ℝ)
    (max ((f : (a : L) → ℝ) (x ^ p.natDegree)) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i)) :
      ℝ)

Tactic:
IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)

Premises used: ne_of_gt, IsNonarchimedean.add_eq_max_of_ne
-- 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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree + ∑ x_1 ∈ Finset.range p.natDegree, p.coeff x_1 • x ^ x_1) : ℝ)
    (max ((f : (a : L) → ℝ) (x ^ p.natDegree)) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i)) :
      ℝ)

Tactic:
exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)

Premises used: ne_of_gt, IsNonarchimedean.add_eq_max_of_ne
-- 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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)

Tactic:
have h_eq : f 0 = f (x ^ p.natDegree) := by
        rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree,
          one_smul, ← max_eq_left_of_lt h_lt]
        exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
h_eq : Eq (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ Ne (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
h_eq ▸ ne_of_gt (lt_of_le_of_lt (apply_nonneg _ _) h_lt)

Premises used: lt_of_le_of_lt, Eq.rec, ne_of_gt, NonnegHomClass.apply_nonneg, Eq.symm
-- 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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
h_eq : Eq (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ Ne (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
exact h_eq ▸ ne_of_gt (lt_of_le_of_lt (apply_nonneg _ _) h_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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ Ne (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
have h0 : f 0 ≠ 0 := by
      have h_eq : f 0 = f (x ^ p.natDegree) := by
        rw [← hx, aeval_eq_sum_range, Finset.sum_range_succ, add_comm, hp.coeff_natDegree,
          one_smul, ← max_eq_left_of_lt h_lt]
        exact IsNonarchimedean.add_eq_max_of_ne hf_na (ne_of_gt h_lt)
      exact h_eq ▸ ne_of_gt (lt_of_le_of_lt (apply_nonneg _ _) h_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
hn_lt : ∀ (n : ℕ) (hn : n < p.natDegree), ‖p.coeff n‖ < HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (p.natDegree - n)
h_deg : 0 < p.natDegree
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
h0 : Ne (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ False

Tactic:
h0 (map_zero _)

Premises used: map_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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
h0 : Ne (α := ℝ) ((f : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ False

Tactic:
exact h0 (map_zero _)

Premises used: map_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
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
apply : ∀ (x : L), LE.le (α := ℝ) (0 : ℝ) (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)
⊢ LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)

Tactic:
apply iSup_nonneg (fun _ ↦ ?_)

Premises used: Real.iSup_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
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
x : L
pos : x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) x : ℝ)
neg : x ∉ s → LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) (0 : ℝ) (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)

Tactic:
split_ifs
-- 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
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
x : L
h : x ∈ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) x : ℝ)

Tactic:
apply_nonneg _ _

Premises used: NonnegHomClass.apply_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
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
x : L
h : x ∉ s
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_refl _

Premises used: le_refl