awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
⊢ 0 ≠ spectralNorm K L y
have rw : ¬minpoly K y = HPow.hPow (α := K[X]) X (natDegree (minpoly K y))
Tactic: rw [spectralNorm, ne_eq, eq_comm, spectralValue_eq_zero_iff (minpoly.monic hy_alg.isIntegral)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = HPow.hPow (α := K[X]) X (natDegree (minpoly K y))
⊢ False
have apply : coeff (minpoly K y) 0 = 0
Tactic: apply minpoly.coeff_zero_ne_zero hy_alg.isIntegral hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
h : minpoly K y = HPow.hPow (α := K[X]) X (natDegree (minpoly K y))
⊢ coeff (minpoly K y) 0 = 0
have rw : (HPow.hPow (α := K[X]) X (natDegree (minpoly K y))).coeff 0 = 0
Tactic: rw [h, coeff_X_pow, if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ coeff (minpoly K y) 0 = 0
have rw₁ : Eq.{u_2 + 1} (α := K) (if 0 = natDegree (minpoly K y) then 1 else 0) 0
Tactic: rw [h, coeff_X_pow, if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ coeff (minpoly K y) 0 = 0
have rw₂ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [h, coeff_X_pow, if_neg (ne_of_lt (minpoly.natDegree_pos hy_alg.isIntegral))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : spectralNorm K L x = 0
hx_alg : IsAlgebraic K x
⊢ x = 0
have by_contra : ∀ (h0 : ¬x = 0), False
Tactic: by_contra h0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) (minpoly K x) : L) (0 : L)
have rw : Eq.{u_3 + 1} (α := L) 0 0
Tactic: rw [minpoly.aeval]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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 : ℝ)
have rw : Norm.norm.{u_2} (E := K) 1 = 1
Tactic: rw [← (algebraMap K L).map_one, hf_ext]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: have hf1 : f 1 = 1 := by
    rw [← (algebraMap K L).map_one, hf_ext]
    simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
have refine : 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 _))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have hp_sp : Splits (Polynomial.map (algebraMap K L) (minpoly K x))
Tactic: have hp_sp : Splits ((minpoly K x).map (algebraMap K L)) := hn.splits x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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))
⊢ spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have 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)
Tactic: obtain ⟨s, hs⟩ := splits_iff_exists_multiset.mp hp_sp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
have rw : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) 1 : L) (1 : L)
Tactic: rw [minpoly.monic (hn.isIntegral x), map_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) (leadingCoeff (minpoly K x)) : L) (1 : L)
have rw₁ : Eq.{u_3 + 1} (α := L) 1 1
Tactic: rw [minpoly.monic (hn.isIntegral x), map_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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])
⊢ spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have h_lc : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
⊢ spectralNorm K L x ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have 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))
Tactic: rw [leadingCoeff_map, h_lc, map_one, one_mul] at hs
Cleared hypotheses: hs, h_lc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
⊢ spectralValue.{u_2} (R := K) (minpoly K x) ≤ ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have 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))
Tactic: rw [← max_norm_root_eq_spectralValue hf_pm hf_na hf1 _ _ hs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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)
⊢ 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))
have 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) : ℝ)
Tactic: apply ciSup_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ LE.le (α := ℝ) (if y ∈ s then (f : (a : L) → ℝ) y else 0 : ℝ)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
have pos : ∀ (h : y ∈ s),
  LE.le (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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) : ℝ)
⊢ LE.le (α := ℝ) (if y ∈ s then (f : (a : L) → ℝ) y else 0 : ℝ)
    (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
have neg : ∀ (h : y ∉ s), LE.le (α := ℝ) 0 (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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 (α := ℝ) ((f : (a : L) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
have 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) : ℝ)
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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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) → ℝ) y : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
have pos : LE.le (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
  (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
Tactic: rw [← hσ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have have : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
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 _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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 : ℝ)
⊢ spectralNorm K L x = ⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)
have have₁ : ∀ (hf1 : Eq (α := ℝ) ((f : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)),
  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 _ _