awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
⊢ (f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have 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)) : ℝ)
Tactic: have h : f ((-1) ^ (card s - m) * s.esymm (card s - m)) = f (s.esymm (card s - m)) := by
        rcases neg_one_pow_eq_or L (card s - m) with h1 | hn1
        · rw [h1, one_mul]
        · rw [hn1, neg_mul, one_mul, map_neg_eq_map]
-- 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)) : ℝ)
⊢ (f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have pos : (f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤
  HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
Tactic: rw [h, esymm]
-- 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)) : ℝ)
⊢ (f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have pos : ∀ (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 : ℝ)),
  (f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
Tactic: obtain ⟨t, ht_card, hts, ht_ge⟩ : ∃ t : Multiset L, card t = card s - m ∧
          (∀ x : L, x ∈ t → x ∈ s) ∧ f (map prod (powersetCard (card s - m) s)).sum ≤ f t.prod :=
        hf_na.multiset_powerset_image_add s 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 : ℕ
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 : ℝ)
⊢ (f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤
    HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have pos : (f : (a : L) → ℝ) t.prod ≤ HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
Tactic: apply le_trans ht_ge
-- 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 : ℝ)
⊢ (f : (a : L) → ℝ) t.prod ≤ HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
Tactic: have h_pr : f t.prod ≤ (t.map f).prod := le_prod_of_submultiplicative_of_nonneg f
        (apply_nonneg _) (le_of_eq hf1) (map_mul_le_mul _) t
-- 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) : ℝ)
⊢ (f : (a : L) → ℝ) t.prod ≤ HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
have pos : prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤
  HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - m)
Tactic: apply le_trans h_pr
-- 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) : ℝ)
⊢ 0 < s.toFinset.card
have hs0 : 0 < s.card
Tactic: have hs0 : 0 < s.card := hps ▸ hm.pos
-- 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) : ℝ)
hs0 : 0 < s.card
⊢ 0 < s.toFinset.card
have obtain : ∀ (x : L) (hx : x ∈ s), 0 < s.toFinset.card
Tactic: obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp hs0
-- 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) : ℝ)
⊢ 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 hs_ne : s ≠ 0
Tactic: have hs_ne : s ≠ 0 :=
        have hpos : 0 < s.toFinset.card := by
          have hs0 : 0 < s.card := hps ▸ hm.pos
          obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp hs0
          exact Finset.card_pos.mpr ⟨x, mem_toFinset.mpr hx⟩
        toFinset_nonempty.mp (Finset.card_pos.mp hpos)
-- 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
⊢ 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 pos : ∀ (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)
Tactic: obtain ⟨y, hyx, hy_max⟩ : ∃ y : L, y ∈ s ∧ ∀ z : L, z ∈ s → f z ≤ f y :=
        exists_max_image f hs_ne
-- 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) ⋯
⊢ p.natDegree - m = (Multiset.map g t).card
have rw : p.natDegree - m = t.card
Tactic: rw [card_map, ht_card, ← hps]
-- 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) ⋯
rw : p.natDegree - m = t.card
⊢ p.natDegree - m = (Multiset.map g t).card
have rw₁ : p.natDegree - m = s.card - m
Tactic: rw [card_map, ht_card, ← hps]
-- 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) ⋯
rw : p.natDegree - m = t.card
rw₁ : p.natDegree - m = s.card - m
⊢ p.natDegree - m = (Multiset.map g t).card
have rw₂ : s.card - m = s.card - m
Tactic: rw [card_map, ht_card, ← hps]
-- 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) ⋯
⊢ prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)
have h_card : p.natDegree - m = (Multiset.map g t).card
Tactic: have h_card : p.natDegree - m = card (t.map g) := by rw [card_map, ht_card, ← hps]