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
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
x : L
hx_alg : IsAlgebraic K x
rw rw₁ : Eq.{u_3 + 1} (α := L) 0 0
⊢ Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) (minpoly K x) : L) (0 : L)

Tactic:
rw [minpoly.aeval]

Premises used: minpoly.aeval
-- 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
σ : Gal(L/K)
x : L
⊢ spectralNorm K L x = spectralNorm K L ((σ : (a : L) → L) x : L)

Tactic:
simp only [spectralNorm, minpoly.algEquiv_eq]

Premises used: minpoly.algEquiv_eq, 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
rw : Norm.norm.{u_2} (E := K) 1 = 1
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
rw [← (algebraMap K L).map_one, hf_ext]

Premises used: Algebra.algebraMap, RingHom.map_one
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
⊢ Norm.norm.{u_2} (E := K) 1 = 1

Tactic:
simp
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
have hf1 : f 1 = 1 := by
    rw [← (algebraMap K L).map_one, hf_ext]
    simp
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)

Tactic:
le_antisymm ?_ (ciSup_le fun σ ↦
    norm_root_le_spectralValue hf_pm hf_na
      (minpoly.monic (hn.isIntegral x)) (minpoly.aeval_algHom _ σ.toAlgHom _))

Premises used: minpoly.monic, AlgEquiv.toAlgHom, Normal.isIntegral, le_antisymm, minpoly.aeval_algHom, norm_root_le_spectralValue, ciSup_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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
refine : spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
⊢ spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)

Tactic:
refine le_antisymm ?_ (ciSup_le fun σ ↦
    norm_root_le_spectralValue hf_pm hf_na
      (minpoly.monic (hn.isIntegral x)) (minpoly.aeval_algHom _ σ.toAlgHom _))

Premises used: minpoly.monic, Normal.isIntegral, le_antisymm, norm_root_le_spectralValue, ciSup_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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
⊢ Splits (Polynomial.map (algebraMap K L) (minpoly K x))

Tactic:
have hp_sp : Splits ((minpoly K x).map (algebraMap K L)) := hn.splits 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
obtain :
  ∀ (s : Multiset L)
    (hs :
      Polynomial.map (algebraMap K L) (minpoly K x) =
        HMul.hMul (α := L[X]) (β := L[X])
          ((C : (a : L) → L[X]) (leadingCoeff (Polynomial.map (algebraMap K L) (minpoly K x))) : L[X])
          (Multiset.prod
              (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s) :
            L[X])),
    spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
⊢ spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)

Tactic:
obtain ⟨s, hs⟩ := splits_iff_exists_multiset.mp hp_sp

Premises used: Polynomial.splits_iff_exists_multiset, 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    HMul.hMul (α := L[X]) (β := L[X])
      ((C : (a : L) → L[X]) (leadingCoeff (Polynomial.map (algebraMap K L) (minpoly K x))) : L[X])
      (Multiset.prod
          (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s) :
        L[X])
rw : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) 1 : L) (1 : L)
rw₁ rw₂ : Eq.{u_3 + 1} (α := L) 1 1
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)

Tactic:
rw [minpoly.monic (hn.isIntegral x), map_one]

Premises used: minpoly.monic, Normal.isIntegral, map_one
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    HMul.hMul (α := L[X]) (β := L[X])
      ((C : (a : L) → L[X]) (leadingCoeff (Polynomial.map (algebraMap K L) (minpoly K x))) : L[X])
      (Multiset.prod
          (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s) :
        L[X])
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)

Tactic:
have h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1 := by
      rw [minpoly.monic (hn.isIntegral x), map_one]
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    HMul.hMul (α := L[X]) (β := L[X])
      ((C : (a : L) → L[X]) (leadingCoeff (Polynomial.map (algebraMap K L) (minpoly K x))) : L[X])
      (Multiset.prod
          (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s) :
        L[X])
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
⊢ Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))

Tactic:
rw [leadingCoeff_map, h_lc, map_one, one_mul] at hs

Premises used: map_one, Polynomial.leadingCoeff_map, 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    HMul.hMul (α := L[X]) (β := L[X])
      ((C : (a : L) → L[X]) (leadingCoeff (Polynomial.map (algebraMap K L) (minpoly K x))) : L[X])
      (Multiset.prod
          (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s) :
        L[X])
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
hs₁ :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)

Tactic:
rw [leadingCoeff_map, h_lc, map_one, one_mul] at hs

Premises used: map_one, Polynomial.leadingCoeff_map, 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
rw :
  LE.le (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L))
⊢ spectralValue.{u_2} (R := K) (minpoly K x) ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)

Tactic:
rw [← max_norm_root_eq_spectralValue hf_pm hf_na hf1 _ _ hs]

Premises used: max_norm_root_eq_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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
H :
  ∀ (x_1 : L),
    LE.le (α := ℝ) (if x_1 ∈ s then (f : (a : L) → ℝ) x_1 else 0 : ℝ)
      (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
⊢ LE.le (α := ℝ) (⨆ (x : L), if x ∈ s then (f : (a : L) → ℝ) x else 0)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L))

Tactic:
apply ciSup_le

Premises used: ciSup_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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
pos :
  ∀ (h : y ∈ s),
    LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
neg : ∀ (h : y ∉ s), LE.le (α := ℝ) 0 (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L))
⊢ LE.le (α := ℝ) (if y ∈ s then (f : (a : L) → ℝ) y else 0 : ℝ)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)

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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
h : y ∈ s
⊢ ∃ (σ : Gal(L/K)), (σ : (a : L) → L) x = y

Tactic:
minpoly.exists_algEquiv_of_root'
        (Algebra.IsAlgebraic.isAlgebraic x) (aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)

Premises used: Algebra.IsAlgebraic.isAlgebraic, minpoly.exists_algEquiv_of_root', Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
h : y ∈ s
pos :
  ∀ (σ : Gal(L/K)) (hσ : (σ : (a : L) → L) x = y),
    LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)

Tactic:
obtain ⟨σ, hσ⟩ : ∃ σ : Gal(L/K), σ x = y := minpoly.exists_algEquiv_of_root'
        (Algebra.IsAlgebraic.isAlgebraic x) (aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)

Premises used: Algebra.IsAlgebraic.isAlgebraic, minpoly.exists_algEquiv_of_root', Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
h : y ∈ s
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
pos :
  LE.le (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)

Tactic:
rw [← 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
h : y ∈ s
σ : Gal(L/K)
hσ : (σ : (a : L) → L) x = y
⊢ LE.le (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)

Tactic:
apply Finite.le_ciSup _ σ

Premises used: Finite.le_ciSup
-- 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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
h : y ∉ s
⊢ LE.le (α := ℝ) 0 (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L))

Tactic:
iSup_nonneg fun σ ↦ apply_nonneg _ _

Premises used: NonnegHomClass.apply_nonneg, DFunLike.coe, Real.iSup_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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
p : K[X] := minpoly K x
hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
s : Multiset L
hs :
  Eq (α := L[X]) (Polynomial.map (algebraMap K L) (minpoly K x))
    (Multiset.prod (Multiset.map (fun (x : L) ↦ HSub.hSub (α := L[X]) (β := L[X]) X ((C : (a : L) → L[X]) x : L[X])) s))
h_lc : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
y : L
h : y ∉ s
⊢ LE.le (α := ℝ) 0 (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L))

Tactic:
exact iSup_nonneg fun σ ↦ apply_nonneg _ _

Premises used: NonnegHomClass.apply_nonneg, Real.iSup_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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
have : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
have₁ :
  ∀ (hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)),
    spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have₂ : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
have₃ have₄ :
  ∀ (hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)),
    spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have₅ :
  ∀ (hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)),
    spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
⊢ spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)

Tactic:
classical
  have hf1 : f 1 = 1 := by
    rw [← (algebraMap K L).map_one, hf_ext]
    simp
  refine le_antisymm ?_ (ciSup_le fun σ ↦
    norm_root_le_spectralValue hf_pm hf_na
      (minpoly.monic (hn.isIntegral x)) (minpoly.aeval_algHom _ σ.toAlgHom _))
  · set p := minpoly K x
    have hp_sp : Splits ((minpoly K x).map (algebraMap K L)) := hn.splits x
    obtain ⟨s, hs⟩ := splits_iff_exists_multiset.mp hp_sp
    have h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1 := by
      rw [minpoly.monic (hn.isIntegral x), map_one]
    rw [leadingCoeff_map, h_lc, map_one, one_mul] at hs
    simp only [spectralNorm]
    rw [← max_norm_root_eq_spectralValue hf_pm hf_na hf1 _ _ hs]
    apply ciSup_le
    intro y
    split_ifs with h
    · obtain ⟨σ, hσ⟩ : ∃ σ : Gal(L/K), σ x = y := minpoly.exists_algEquiv_of_root'
        (Algebra.IsAlgebraic.isAlgebraic x) (aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)
      rw [← hσ]
      apply Finite.le_ciSup _ σ
    · exact iSup_nonneg fun σ ↦ apply_nonneg _ _

Premises used: minpoly.monic, spectralNorm, minpoly, Normal.isIntegral, le_antisymm, norm_root_le_spectralValue, map_one, Polynomial.leadingCoeff_map, NonnegHomClass.apply_nonneg, ciSup_le, one_mul, Real.iSup_nonneg