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
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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
g : L → NNReal := fun (x : L) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((f : (a : L) → ℝ) x) ⋯
h_card : p.natDegree - m = (Multiset.map g t).card
r : NNReal
hr : r ∈ Multiset.map g t
⊢ r ≤ g y
have obtain : ∀ (w : L) (hzt : w ∈ t) (hzr : g w = r), r ≤ g y
Tactic: obtain ⟨_, hzt, hzr⟩ := mem_map.mp hr
-- 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
h_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
g : L → NNReal := fun (x : L) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((f : (a : L) → ℝ) x) ⋯
h_card : p.natDegree - m = (Multiset.map g t).card
⊢ prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
have hx_le : ∀ x ∈ Multiset.map g t, x ≤ g y
Tactic: have hx_le : ∀ x : NNReal, x ∈ map g t → x ≤ g y := by
          intro r hr
          obtain ⟨_, hzt, hzr⟩ := mem_map.mp hr
          exact hzr ▸ hy_max _ (hts _ hzt)
-- 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
h_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
g : L → NNReal := fun (x : L) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((f : (a : L) → ℝ) x) ⋯
h_card : p.natDegree - m = (Multiset.map g t).card
hx_le : ∀ x ∈ Multiset.map g t, x ≤ g y
⊢ prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
have this : (Multiset.map g t).prod ≤ g y ^ (p.natDegree - m)
Tactic: have : (map g t).prod ≤ g y ^ (p.natDegree - m) := h_card ▸ prod_le_pow_card _ _ hx_le
-- 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
h_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
⊢ prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
Tactic: have : (map f t).prod ≤ f y ^ (p.natDegree - m) := by
        set g : L → NNReal := fun x ↦ ⟨f x, apply_nonneg f x⟩
        have h_card : p.natDegree - m = card (t.map g) := by rw [card_map, ht_card, ← hps]
        have hx_le : ∀ x : NNReal, x ∈ map g t → x ≤ g y := by
          intro r hr
          obtain ⟨_, hzt, hzr⟩ := mem_map.mp hr
          exact hzr ▸ hy_max _ (hts _ hzt)
        have : (map g t).prod ≤ g y ^ (p.natDegree - m) := h_card ▸ prod_le_pow_card _ _ hx_le
        simpa [g, ← NNReal.coe_le_coe, NNReal.coe_pow, NNReal.coe_mk, NNReal.coe_multiset_prod,
          map_map, Function.comp_apply, NNReal.coe_mk] using this
-- 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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
⊢ BddAbove (α := ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0)
have h₁ : Membership.mem (α := ℝ) (γ := Set ℝ) (upperBounds (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0))
  ((f : (a : L) → ℝ) y : ℝ)
Tactic: use f y
-- 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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0) r
⊢ r ≤ (f : (a : L) → ℝ) y
have h₁ : ∀ (z : L) (hz : (fun (x : L) ↦ (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)) z = r), r ≤ (f : (a : L) → ℝ) y
Tactic: obtain ⟨z, hz⟩ := Set.mem_range.mpr hr
-- 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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0) r
z : L
hz : (if z ∈ s then (f : (a : L) → ℝ) z else 0) = r
⊢ r ≤ (f : (a : L) → ℝ) y
have h₁ : LE.le (α := ℝ) (if z ∈ s then (f : (a : L) → ℝ) z else 0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)
Tactic: rw [← hz]
-- 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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0) r
z : L
hz : (if z ∈ s then (f : (a : L) → ℝ) z else 0) = r
⊢ LE.le (α := ℝ) (if z ∈ s then (f : (a : L) → ℝ) z else 0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)
have pos : ∀ (h : z ∈ s), LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
Tactic: split_ifs with h
-- 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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0) r
z : L
hz : (if z ∈ s then (f : (a : L) → ℝ) z else 0) = r
pos : ∀ (h : z ∈ s), LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) (if z ∈ s then (f : (a : L) → ℝ) z else 0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)
have neg : ∀ (h : z ∉ s), LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)
Tactic: split_ifs with 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
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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
⊢ prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have h_bdd : BddAbove (α := ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0)
Tactic: have h_bdd : BddAbove (Set.range fun x : L ↦ ite (x ∈ s) (f x) 0) := by
        use f y
        intro r hr
        obtain ⟨z, hz⟩ := Set.mem_range.mpr hr
        simp only at hz
        rw [← hz]
        split_ifs with h
        · exact hy_max _ h
        · exact apply_nonneg _ _
-- 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_1 : 0 < HSub.hSub (α := ℝ) (↑p.natDegree : ℝ) (↑m : ℝ)
hps : s.card = p.natDegree
hc :
  ‖p.coeff m‖ = (f : (a : L) → ℝ) (coeff (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p) m)
h :
  Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
    ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
    ((f : (a : L) → ℝ) t.prod : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)
this : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
h_bdd : BddAbove (α := ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0)
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (if y ∈ s then (f : (a : L) → ℝ) y else 0 : ℝ)
have rw : LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) ((f : (a : L) → ℝ) y : ℝ)
Tactic: rw [if_pos hyx]
-- 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
E : Type u_4
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Algebra E L
inst_6 : IsScalarTower K E L
x : E
⊢ spectralNorm K E x = spectralNorm.{u_2, u_3} K L ((algebraMap E L : (a : E) → L) x : L)
have hx : Eq (α := K[X]) (minpoly.{u_2, u_3} K (B := L) ((algebraMap E L : (a : E) → L) x : L)) (minpoly K x)
Tactic: have hx : minpoly K (algebraMap E L x) = minpoly K x :=
    minpoly.algebraMap_eq (algebraMap E L).injective 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
⊢ spectralValue.{u_2} (R := K) (minpoly.{u_2, u_3} K (B := L) 0) = 0
have rw : spectralValue.{u_2} (R := K) X = 0
Tactic: rw [minpoly.zero, ← pow_one X, spectralValue_X_pow 1]
-- 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
rw : spectralValue.{u_2} (R := K) X = 0
⊢ spectralValue.{u_2} (R := K) (minpoly.{u_2, u_3} K (B := L) 0) = 0
have rw₁ : spectralValue.{u_2} (R := K) (HPow.hPow (α := K[X]) (β := ℕ) X 1) = 0
Tactic: rw [minpoly.zero, ← pow_one X, spectralValue_X_pow 1]
-- 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
rw : spectralValue.{u_2} (R := K) X = 0
rw₁ : spectralValue.{u_2} (R := K) (HPow.hPow (α := K[X]) (β := ℕ) X 1) = 0
⊢ spectralValue.{u_2} (R := K) (minpoly.{u_2, u_3} K (B := L) 0) = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [minpoly.zero, ← pow_one X, spectralValue_X_pow 1]
-- 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
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
⊢ 0 < spectralNorm K L y
have apply : 0 ≠ spectralNorm K L y
Tactic: apply lt_of_le_of_ne (spectralNorm_nonneg _)