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
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
⊢ LT.lt (α := ℝ) ((f : (a : L) → ℝ) ((Finset.range p.natDegree).sum g) : ℝ) ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
have 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) : ℝ)
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⟩
-- 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
⊢ False
have h_lt : 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))
-- 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
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) : ℝ)
have 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)) :
    ℝ)
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]
-- 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
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 : ℝ)
have h_eq : 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)
-- 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
h_lt :
  LT.lt (α := ℝ) ((f : (a : L) → ℝ) (∑ i ∈ Finset.range p.natDegree, p.coeff i • x ^ i) : ℝ)
    ((f : (a : L) → ℝ) (x ^ p.natDegree) : ℝ)
⊢ False
have h0 : 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)
-- 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
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])
⊢ LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
have apply : ∀ (x : L), LE.le (α := ℝ) (0 : ℝ) (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)
Tactic: apply iSup_nonneg (fun _ ↦ ?_)
-- 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
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
⊢ LE.le (α := ℝ) (0 : ℝ) (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)
have pos : x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) x : ℝ)
Tactic: split_ifs
-- 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
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 : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)
have neg : x ∉ s → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- 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
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), if x ∈ s then (f : (a : L) → ℝ) x else 0) = spectralValue.{u_2} (R := K) p
have h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
Tactic: have h_le : 0 ≤ ⨆ x : L, ite (x ∈ s) (f x) 0 := by
    apply iSup_nonneg (fun _ ↦ ?_)
    split_ifs
    exacts [apply_nonneg _ _, le_refl _]
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
⊢ (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) = spectralValue.{u_2} (R := K) p
have a : (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
Tactic: apply le_antisymm
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
a : (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
⊢ (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) = spectralValue.{u_2} (R := K) p
have a₁ : spectralValue.{u_2} (R := K) p ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
Tactic: apply le_antisymm
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
⊢ (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
have apply : ∀ (x : L), (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
Tactic: apply ciSup_le (fun x ↦ ?_)
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
x : L
⊢ (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
have pos : ∀ (hx : x ∈ s), (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
Tactic: by_cases hx : x ∈ s
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
x : L
pos : ∀ (hx : x ∈ s), (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
⊢ (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
have neg : ∀ (hx : x ∉ s), (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
Tactic: by_cases hx : x ∈ s
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
x : L
hx : x ∈ s
⊢ (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
have hx0 : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
Tactic: have hx0 : aeval x p = 0 := aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s hx hp
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
x : L
hx : x ∈ s
hx0 : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
⊢ (if x ∈ s then (f : (a : L) → ℝ) x else 0) ≤ spectralValue.{u_2} (R := K) p
have pos : (f : (a : L) → ℝ) x ≤ spectralValue.{u_2} (R := K) p
Tactic: rw [if_pos 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
⊢ spectralValue.{u_2} (R := K) p ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
have apply : ∀ (m : ℕ), spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
Tactic: apply ciSup_le (fun m ↦ ?_)
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
m : ℕ
⊢ spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
have pos : ∀ (hm : m < p.natDegree), spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
Tactic: by_cases hm : m < p.natDegree
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
m : ℕ
pos :
  ∀ (hm : m < p.natDegree), spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
⊢ spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
have neg : ∀ (hm : ¬m < p.natDegree), spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
Tactic: by_cases hm : m < p.natDegree
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
m : ℕ
hm : m < p.natDegree
⊢ spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
have pos : ‖p.coeff m‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)) ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
Tactic: rw [spectralValueTerms_of_lt_natDegree _ hm]
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
m : ℕ
hm : m < p.natDegree
⊢ ‖p.coeff m‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)) ≤
    ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
have h : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
Tactic: have h : 0 < (p.natDegree - m : ℝ) := by rw [sub_pos, Nat.cast_lt]; exact hm
-- 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
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])
h_le : LE.le (α := ℝ) 0 (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
m : ℕ
hm : m < p.natDegree
h : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
⊢ ‖p.coeff m‖ ^ (1 / HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)) ≤
    ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0
have pos : ‖p.coeff m‖ ≤ HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
Tactic: rw [← rpow_le_rpow_iff (rpow_nonneg (norm_nonneg _) _) h_le h, ← rpow_mul (norm_nonneg _),
        one_div_mul_cancel (ne_of_gt h), rpow_one, ← Nat.cast_sub (le_of_lt hm), rpow_natCast]