awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
inl :
  ∀ (h1 : HPow.hPow (α := L) (-1) (s.card - m) = 1),
    Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
      ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
inr :
  ∀ (hn1 : HPow.hPow (α := L) (-1) (s.card - m) = -1),
    Eq (α := ℝ) ((f : (a : L) → ℝ) (HPow.hPow (α := L) (-1) (s.card - m) * s.esymm (s.card - m)) : ℝ)
      ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
⊢ 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:
rcases neg_one_pow_eq_or L (card s - m) with h1 | hn1

Premises used: HSub.hSub, Multiset.card, neg_one_pow_eq_or
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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)
h1 : HPow.hPow (α := L) (-1) (s.card - m) = 1
inl : Eq (α := ℝ) ((f : (a : L) → ℝ) (1 * s.esymm (s.card - m)) : ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
inl₁ inl₂ : Eq (α := ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
⊢ 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:
rw [h1, one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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)
hn1 : HPow.hPow (α := L) (-1) (s.card - m) = -1
inr : Eq (α := ℝ) ((f : (a : L) → ℝ) (-1 * s.esymm (s.card - m)) : ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
inr₁ : Eq (α := ℝ) ((f : (a : L) → ℝ) (-(1 * s.esymm (s.card - m))) : ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
inr₂ : Eq (α := ℝ) ((f : (a : L) → ℝ) (-s.esymm (s.card - m)) : ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
inr₃ inr₄ : Eq (α := ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ) ((f : (a : L) → ℝ) (s.esymm (s.card - m)) : ℝ)
⊢ 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:
rw [hn1, neg_mul, one_mul, map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map, neg_mul, one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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)
⊢ 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]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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)) : ℝ)
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)
⊢ (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)

Tactic:
rw [h, esymm]

Premises used: Multiset.esymm
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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),
    t.card = s.card - m ∧
      (∀ x ∈ t, x ∈ s) ∧
        LE.le (α := ℝ) ((f : (a : L) → ℝ) (Multiset.map prod (powersetCard (s.card - m) s)).sum : ℝ)
          ((f : (a : L) → ℝ) t.prod : ℝ)

Tactic:
hf_na.multiset_powerset_image_add s m

Premises used: IsNonarchimedean.multiset_powerset_image_add
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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)) : ℝ)
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)
⊢ (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

Premises used: Multiset.sum, IsNonarchimedean.multiset_powerset_image_add, Multiset.map, Multiset.prod, HSub.hSub, Multiset, Multiset.card, Multiset.powersetCard, 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
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 : ℝ)
pos :
  (f : (a : L) → ℝ) t.prod ≤ HPow.hPow (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0) (p.natDegree - 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)

Tactic:
apply le_trans ht_ge

Premises used: le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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 : ℝ)
⊢ 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
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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) : ℝ)
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)
⊢ (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 h_pr

Premises used: le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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.card

Tactic:
have hs0 : 0 < s.card := hps ▸ hm.pos
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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
obtain : ∀ (x : L) (hx : x ∈ s), 0 < s.toFinset.card
⊢ 0 < s.toFinset.card

Tactic:
obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp hs0

Premises used: Iff.mp, Multiset.card_pos_iff_exists_mem
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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
x : L
hx : x ∈ s
⊢ 0 < s.toFinset.card

Tactic:
Finset.card_pos.mpr ⟨x, mem_toFinset.mpr hx⟩

Premises used: Iff.mpr, Exists.intro, Finset.card_pos, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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
x : L
hx : x ∈ s
⊢ 0 < s.toFinset.card

Tactic:
exact Finset.card_pos.mpr ⟨x, mem_toFinset.mpr hx⟩

Premises used: Iff.mpr, Exists.intro, Finset.card_pos, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X]
s : Multiset L
hp :
  Eq (α := L[X]) (((mapAlg K L : AlgHom.{u_2, u_2, u_3} K K[X] L[X]) : (a : K[X]) → L[X]) p : L[X])
    (prod (Multiset.map (fun (a : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) a : L[X])) s) : L[X])
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) : ℝ)
⊢ 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)