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 : 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
h₁ : LE.le (α := ℝ) (if z ∈ s then (f : (a : L) → ℝ) z else 0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)
⊢ r ≤ (f : (a : L) → ℝ) y

Tactic:
rw [← hz]
-- 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
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 : ℝ)
neg : ∀ (h : z ∉ s), LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) (if z ∈ s then (f : (a : L) → ℝ) z else 0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)

Tactic:
split_ifs with h
-- 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_2 :
  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
h : z ∈ s
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)

Tactic:
hy_max _ h
-- 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_2 :
  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
h : z ∈ s
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) z : ℝ) ((f : (a : L) → ℝ) y : ℝ)

Tactic:
exact hy_max _ h
-- 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_2 :
  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
h : z ∉ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)

Tactic:
apply_nonneg _ _

Premises used: NonnegHomClass.apply_nonneg
-- 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_2 :
  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
h : z ∉ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : L) → ℝ) y : ℝ)

Tactic:
exact apply_nonneg _ _

Premises used: NonnegHomClass.apply_nonneg
-- 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)
⊢ 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 _ _
-- 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_bdd : BddAbove (α := ℝ) (Set.range fun (x : L) ↦ if x ∈ s then (f : (a : L) → ℝ) x else 0)
rw rw₁ : LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) ((f : (a : L) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (if y ∈ s then (f : (a : L) → ℝ) y else 0 : ℝ)

Tactic:
rw [if_pos hyx]

Premises used: if_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) : ℝ)
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)
⊢ 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:
exact le_trans this (pow_le_pow_left₀ (apply_nonneg _ _)
        (le_trans (by rw [if_pos hyx]) (le_ciSup h_bdd y)) _)

Premises used: pow_le_pow_left₀, le_ciSup, NonnegHomClass.apply_nonneg, 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
⊢ spectralValueTerms.{u_2} (R := K) p m ≤ ⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0

Tactic:
simp only [spectralValueTerms, if_neg hm, h_le]

Premises used: spectralValueTerms, if_neg
-- 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
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
⊢ 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
-- 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
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
hx : Eq (α := K[X]) (minpoly.{u_2, u_3} K (B := L) ((algebraMap E L : (a : E) → L) x : L)) (minpoly K x)
⊢ spectralNorm K E x = spectralNorm.{u_2, u_3} K L ((algebraMap E L : (a : E) → L) x : L)

Tactic:
simp only [spectralNorm, hx]

Premises used: spectralNorm
-- 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
E : IntermediateField K L
x : ↥E
⊢ spectralNorm K ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))
      ((algebraMap ↥E ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)) :
            (a : ↥E) → ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)))
          x :
        ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))) =
    spectralNorm K L ((algebraMap (↥E) L : (a : ↥E) → L) x : L)

Tactic:
simp_rw [← spectralNorm.eq_of_tower]

Premises used: spectralNorm.eq_of_tower
-- 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
E : IntermediateField K L
x : L
g : ↥E
h_map : (algebraMap (↥E) L : (a : ↥E) → L) g = x
⊢ spectralNorm K ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))
      ((algebraMap ↥E ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)) :
            (a : ↥E) → ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)))
          g :
        ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))) =
    spectralNorm K L x

Tactic:
h_map ▸ spectralNorm.eq_of_normalClosure' E g

Premises used: Eq.rec, spectralNorm.eq_of_normalClosure'
-- 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
rw : spectralValue.{u_2} (R := K) X = 0
rw₁ : spectralValue.{u_2} (R := K) (HPow.hPow (α := K[X]) (β := ℕ) X 1) = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ spectralValue.{u_2} (R := K) (minpoly.{u_2, u_3} K (B := L) 0) = 0

Tactic:
rw [minpoly.zero, ← pow_one X, spectralValue_X_pow 1]

Premises used: pow_one, minpoly.zero, OfNat.ofNat, Polynomial.X, spectralValue_X_pow
-- 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
y : L
⊢ 0 ≤ spectralNorm K L y

Tactic:
le_ciSup_of_le (spectralValueTerms_bddAbove (minpoly K y)) 0 (spectralValueTerms_nonneg _ 0)

Premises used: le_ciSup_of_le, spectralValueTerms_bddAbove, spectralValueTerms_nonneg, spectralNorm, minpoly, OfNat.ofNat, spectralValue
-- 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
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
apply : 0 ≠ spectralNorm K L y
⊢ 0 < spectralNorm K L y

Tactic:
apply lt_of_le_of_ne (spectralNorm_nonneg _)

Premises used: spectralNorm_nonneg, lt_of_le_of_ne
-- 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
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
rw : ¬minpoly K y = HPow.hPow (α := K[X]) X (natDegree (minpoly K y))
⊢ 0 ≠ spectralNorm K L y

Tactic:
rw [spectralNorm, ne_eq, eq_comm, spectralValue_eq_zero_iff (minpoly.monic hy_alg.isIntegral)]

Premises used: minpoly.monic, spectralNorm, eq_comm, ne_eq, IsAlgebraic.isIntegral, spectralValue_eq_zero_iff
-- 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
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = HPow.hPow (α := K[X]) X (natDegree (minpoly K y))
apply : coeff (minpoly K y) 0 = 0
⊢ False

Tactic:
apply minpoly.coeff_zero_ne_zero hy_alg.isIntegral hy

Premises used: minpoly.coeff_zero_ne_zero, IsAlgebraic.isIntegral
-- 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
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = HPow.hPow (α := K[X]) X (natDegree (minpoly K y))
rw : (HPow.hPow (α := K[X]) X (natDegree (minpoly K y))).coeff 0 = 0
rw₁ : Eq.{u_2 + 1} (α := K) (if 0 = natDegree (minpoly K y) then 1 else 0) 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := K) 0 0
⊢ coeff (minpoly K y) 0 = 0

Tactic:
rw [h, coeff_X_pow, if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))]

Premises used: Polynomial.coeff_X_pow, IsAlgebraic.isIntegral, minpoly.natDegree_pos, ne_of_lt, if_neg
-- 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
x : L
hx : spectralNorm K L x = 0
hx_alg : IsAlgebraic K x
by_contra : ∀ (h0 : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra h0
-- 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
x : L
hx : spectralNorm K L x = 0
hx_alg : IsAlgebraic K x
h0 : ¬x = 0
⊢ False

Tactic:
(ne_of_gt (spectralNorm_zero_lt h0 hx_alg)) hx

Premises used: ne_of_gt, spectralNorm_zero_lt
-- 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
x : L
hx : spectralNorm K L x = 0
hx_alg : IsAlgebraic K x
h0 : ¬x = 0
⊢ False

Tactic:
exact (ne_of_gt (spectralNorm_zero_lt h0 hx_alg)) hx

Premises used: ne_of_gt, spectralNorm_zero_lt