awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
simp_rw :
  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
⊢ Eq (α := ℝ)
    (⨆ (n_1 : ℕ),
      if n_1 < (HPow.hPow (α := R[X]) X n).natDegree then
        ‖(HPow.hPow (α := R[X]) X n).coeff n_1‖ ^
          (1 / HSub.hSub (α := ℝ) (↑(HPow.hPow (α := R[X]) X n).natDegree : ℝ) (↑n_1 : ℝ))
      else 0)
    0

Tactic:
simp_rw [coeff_X_pow n, natDegree_X_pow]

Premises used: Polynomial.coeff_X_pow, Polynomial.natDegree_X_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
⊢ Eq (α := ℝ) (⨆ (x : ℕ), 0) 0

Tactic:
ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
convert_4 : Nonempty ℕ
⊢ 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

Tactic:
convert! ciSup_const using 2

Premises used: ciSup_const
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
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
⊢ 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

Tactic:
ext m
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
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
⊢ (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
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
hmn : m < n
pos : Eq (α := ℝ) 0 0 ∧ ¬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

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]

Premises used: inv_eq_zero, Nat.cast_sub, Nat.sub_eq_zero_iff_le, norm_zero, Real.rpow_eq_zero_iff_of_nonneg, le_of_lt, if_pos, ne_eq, Nat.cast_eq_zero, one_div, ne_of_lt, if_neg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
hmn : m < n
⊢ Eq (α := ℝ) 0 0 ∧ ¬n ≤ m

Tactic:
⟨Eq.refl _, not_le_of_gt hmn⟩

Premises used: And.intro, Eq.refl, not_le_of_gt
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
hmn : m < n
⊢ Eq (α := ℝ) 0 0 ∧ ¬n ≤ m

Tactic:
exact ⟨Eq.refl _, not_le_of_gt hmn⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n m : ℕ
hmn : ¬m < n
neg neg₁ : Eq (α := ℝ) 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

Tactic:
rw [if_neg hmn]

Premises used: if_neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : Nontrivial R
n : ℕ
⊢ Nonempty ℕ

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ spectralValue_X_pow p.natDegree⟩

Premises used: Eq.rec, Iff.intro, Polynomial.natDegree, Eq.symm, spectralValue_X_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
refine : ∀ (h : spectralValue.{u_1} (R := R) p = 0), p = HPow.hPow (α := R[X]) X p.natDegree
⊢ 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⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

Tactic:
hp.eq_X_pow_iff_natDegree_le_natTrailingDegree.mpr <|
    le_natTrailingDegree hp.ne_zero fun n hn ↦ ?_

Premises used: Iff.mpr, Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree, Polynomial.le_natTrailingDegree, Polynomial.Monic.ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
refine : ∀ (n : ℕ) (hn : n < p.natDegree), p.coeff n = 0
⊢ p = HPow.hPow (α := R[X]) X p.natDegree

Tactic:
refine hp.eq_X_pow_iff_natDegree_le_natTrailingDegree.mpr <|
    le_natTrailingDegree hp.ne_zero fun n hn ↦ ?_

Premises used: Iff.mpr, Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree, Polynomial.le_natTrailingDegree, Polynomial.Monic.ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
apply : 0 ≤ spectralValueTerms.{u_1} (R := R) p n
⊢ spectralValueTerms.{u_1} (R := R) p n = 0

Tactic:
apply le_antisymm ((le_ciSup (spectralValueTerms_bddAbove p) n).trans h.le)

Premises used: spectralValueTerms_bddAbove, Eq.le, le_antisymm, le_ciSup, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ 0 ≤ spectralValueTerms.{u_1} (R := R) p n

Tactic:
spectralValueTerms_nonneg _ _

Premises used: spectralValueTerms_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ 0 ≤ spectralValueTerms.{u_1} (R := R) p n

Tactic:
exact spectralValueTerms_nonneg _ _

Premises used: spectralValueTerms_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

Tactic:
have h0 : spectralValueTerms p n = 0 := by
    apply le_antisymm ((le_ciSup (spectralValueTerms_bddAbove p) n).trans h.le)
    exact spectralValueTerms_nonneg _ _
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 ∧ 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

Premises used: Real.rpow_eq_zero_iff_of_nonneg, spectralValueTerms_of_lt_natDegree, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ‖p.coeff n‖ = 0 ∧ 1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) ≠ 0
⊢ p.coeff n = 0

Tactic:
norm_eq_zero.mp h0.1

Premises used: norm_eq_zero, And.left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ‖p.coeff n‖ = 0 ∧ 1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ) ≠ 0
⊢ p.coeff n = 0

Tactic:
exact norm_eq_zero.mp h0.1

Premises used: norm_eq_zero, And.left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

Tactic:
⟨fun h n ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
refine_2 : ∀ (h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1), iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1
⊢ iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1

Tactic:
refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
refine_1₂ : ∀ (hPn : n < P.natDegree), ‖P.coeff n‖ ≤ 1
⊢ ‖P.coeff n‖ ≤ 1

Tactic:
obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n

Premises used: Polynomial.natDegree, lt_trichotomy
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hPn]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
refine_1₂ refine_1₃ : LE.le (α := ℝ) 1 1
⊢ ‖P.coeff n‖ ≤ 1

Tactic:
rw [← hPn, hP.coeff_natDegree, norm_one]

Premises used: NormOneClass.norm_one, Polynomial.Monic.coeff_natDegree
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ spectralValueTerms.{u_1} (R := R) P n ≤ 1

Tactic:
have : spectralValueTerms P n ≤ 1 := le_ciSup (spectralValueTerms_bddAbove P) n |>.trans h
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
refine_1 : ∀ (this : 1 < ‖P.coeff n‖), 1 < spectralValueTerms.{u_1} (R := R) P n
⊢ ‖P.coeff n‖ ≤ 1

Tactic:
contrapose! this
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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‖
refine_1 : 1 < ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ))
⊢ 1 < spectralValueTerms.{u_1} (R := R) P n

Tactic:
simp only [spectralValueTerms_of_lt_natDegree _ hPn]

Premises used: spectralValueTerms_of_lt_natDegree
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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‖
⊢ 0 < 1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)

Tactic:
simp [hPn]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 < ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ))

Tactic:
exact Real.one_lt_rpow this (by simp [hPn])

Premises used: Real.one_lt_rpow
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
inst : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
apply : ∀ (n : ℕ), spectralValueTerms.{u_1} (R := R) P n ≤ 1
⊢ iSup (spectralValueTerms.{u_1} (R := R) P) ≤ 1

Tactic:
apply ciSup_le (fun n ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
neg : ∀ (hn : ¬n < P.natDegree), LE.le (α := ℝ) 0 1
⊢ (if n < P.natDegree then ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) else 0) ≤ 1

Tactic:
split_ifs with hn
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
pos : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)
⊢ ‖P.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)) ≤ 1

Tactic:
apply Real.rpow_le_one (norm_nonneg _) (h n)

Premises used: Real.rpow_le_one, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
pos : n ≤ P.natDegree
⊢ 0 ≤ 1 / HSub.hSub (α := ℝ) (↑P.natDegree : ℝ) (↑n : ℝ)

Tactic:
rw [one_div_nonneg, sub_nonneg, Nat.cast_le]

Premises used: one_div_nonneg, Nat.cast_le, sub_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ n ≤ P.natDegree

Tactic:
le_of_lt hn

Premises used: le_of_lt
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ n ≤ P.natDegree

Tactic:
exact le_of_lt hn

Premises used: le_of_lt
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- 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)
pos : ∀ (hx0 : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (0 : ℝ)), (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
neg : ∀ (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

Tactic:
by_cases hx0 : f x = 0

Premises used: DFunLike.coe
-- 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 : ℝ)
pos : 0 ≤ spectralValue.{u_2} (R := K) p
⊢ (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p

Tactic:
rw [hx0]
-- 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 : ℝ)
⊢ 0 ≤ spectralValue.{u_2} (R := K) p

Tactic:
spectralValue_nonneg p

Premises used: spectralValue_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 : ℝ)
⊢ 0 ≤ spectralValue.{u_2} (R := K) p

Tactic:
exact spectralValue_nonneg p

Premises used: spectralValue_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 : ℝ)
neg : ∀ (h_ge : ¬(f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p), False
⊢ (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p

Tactic:
by_contra h_ge
-- 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
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‖
rw₇ rw₈ : ‖p.coeff n‖ = ‖p.coeff n‖
⊢ (‖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))]

Premises used: Nat.cast_sub, le_of_lt, ne_of_gt, Real.pow_rpow_inv_natCast, one_div, mul_comm, Real.rpow_mul, norm_nonneg, Real.rpow_natCast, 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‖ ^ (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))]
-- 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‖
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
⊢ ‖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

Premises used: not_le, iSup, spectralValueTerms, Set.Finite.csSup_lt_iff, spectralValueTerms_finite_range, Set.range_nonempty, spectralValue
-- 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 : spectralValueTerms.{u_2} (R := K) p n = ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))
⊢ ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ)) ∈ Set.range (spectralValueTerms.{u_2} (R := K) p)

Tactic:
use n
-- 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‖
⊢ spectralValueTerms.{u_2} (R := K) p n = ‖p.coeff n‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑n : ℝ))

Tactic:
simp only [spectralValueTerms, if_pos hn]

Premises used: spectralValueTerms, if_pos