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_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 ∈ s, ∀ z ∈ s, LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)

Tactic:
exists_max_image f hs_ne

Premises used: Multiset.exists_max_image, 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 : ℝ)
h_pr : LE.le (α := ℝ) ((f : (a : L) → ℝ) t.prod : ℝ) (prod (Multiset.map (⇑f : (a : L) → ℝ) t) : ℝ)
hs_ne : s ≠ 0
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)
⊢ 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

Premises used: Multiset.exists_max_image, 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 : ℝ)
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
rw₂ rw₃ : s.card - m = s.card - m
⊢ p.natDegree - m = (Multiset.map g t).card

Tactic:
rw [card_map, ht_card, ← hps]

Premises used: Multiset.card_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)) : ℝ)
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

Tactic:
have h_card : p.natDegree - m = card (t.map g) := by rw [card_map, ht_card, ← hps]
-- 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) : ℝ)
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
obtain : ∀ (w : L) (hzt : w ∈ t) (hzr : g w = r), r ≤ g y
⊢ r ≤ g y

Tactic:
obtain ⟨_, hzt, hzr⟩ := mem_map.mp hr

Premises used: Multiset.mem_map, Iff.mp
-- 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) : ℝ)
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
w : L
hzt : w ∈ t
hzr : g w = r
⊢ r ≤ g y

Tactic:
hzr ▸ hy_max _ (hts _ hzt)

Premises used: Eq.rec
-- 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) : ℝ)
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
w : L
hzt : w ∈ t
hzr : g w = r
⊢ r ≤ g y

Tactic:
exact hzr ▸ hy_max _ (hts _ hzt)
-- 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) : ℝ)
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
⊢ ∀ 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)
-- 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) : ℝ)
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
⊢ (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
-- 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) : ℝ)
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
this : (Multiset.map g t).prod ≤ g y ^ (p.natDegree - m)
⊢ prod (Multiset.map (⇑f : (a : L) → ℝ) t) ≤ HPow.hPow (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (p.natDegree - m)

Tactic:
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

Premises used: NNReal.coe_multiset_prod, NNReal.coe_mk, NNReal.coe_pow, Multiset.map_map, Function.comp_apply, NNReal.coe_le_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 : ℝ)
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 (α := ℝ) ((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
-- 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) : ℝ)
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₁ :
  Membership.mem (α := ℝ) (γ := Set ℝ) (upperBounds (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0))
    ((f : (a : L) → ℝ) y : ℝ)
⊢ BddAbove (α := ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0)

Tactic:
use f y

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
h₁ : ∀ (z : L) (hz : (fun (x : L) ↦ (if x ∈ s then (f : (a : L) → ℝ) x else 0 : ℝ)) z = r), r ≤ (f : (a : L) → ℝ) y
⊢ r ≤ (f : (a : L) → ℝ) y

Tactic:
obtain ⟨z, hz⟩ := Set.mem_range.mpr hr

Premises used: Iff.mpr, Set.mem_range