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
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)
⊢ 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 _ _
-- 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
hu : IsUltrametricDist K
⊢ spectralNorm K L = (⇑(invariantExtension K L) : (a : L) → ℝ)
have h : ∀ (x : L), spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
Tactic: ext x
-- 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
hu : IsUltrametricDist K
x : L
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
have hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
Tactic: have hna := hu.isNonarchimedean_norm
-- 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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
have hf : let f :=
  Classical.choose (p := fun (x : AlgebraNorm K L) ↦
    IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
      (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
    sorry;
f =
  Classical.choose (p := fun (x : AlgebraNorm K L) ↦
    IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
      (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
    sorry
Tactic: set f := Classical.choose (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)
    with hf
-- 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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
f : AlgebraNorm K L :=
  Classical.choose (p := fun (x : AlgebraNorm K L) ↦
    IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
      (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
    ⋯
hf :
  f =
    Classical.choose (p := fun (x : AlgebraNorm K L) ↦
      IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
        (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
          IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
      ⋯
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
have hf_pow : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
Tactic: have hf_pow : IsPowMul f := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).1
-- 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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
f : AlgebraNorm K L :=
  Classical.choose (p := fun (x : AlgebraNorm K L) ↦
    IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
      (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
    ⋯
hf :
  f =
    Classical.choose (p := fun (x : AlgebraNorm K L) ↦
      IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
        (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
          IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
      ⋯
hf_pow : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
have hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
Tactic: have hf_ext : ∀ (x : K), f (algebraMap K L x) = ‖x‖ := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).2.1
-- 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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
f : AlgebraNorm K L :=
  Classical.choose (p := fun (x : AlgebraNorm K L) ↦
    IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
      (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
    ⋯
hf :
  f =
    Classical.choose (p := fun (x : AlgebraNorm K L) ↦
      IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
        (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
          IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
      ⋯
hf_pow : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
have hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
Tactic: have hf_na : IsNonarchimedean f := (Classical.choose_spec
    (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).2.2
-- 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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
f : AlgebraNorm K L :=
  Classical.choose (p := fun (x : AlgebraNorm K L) ↦
    IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
      (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
        IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
    ⋯
hf :
  f =
    Classical.choose (p := fun (x : AlgebraNorm K L) ↦
      IsPowMul (R := L) (⇑x : (a : L) → ℝ) ∧
        (∀ (x_1 : K), (x : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x_1 : L) = ‖x_1‖) ∧
          IsNonarchimedean (R := ℝ) (α := L) (⇑x : (a : L) → ℝ))
      ⋯
hf_pow : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
hf_na : IsNonarchimedean (R := ℝ) (α := L) (⇑f : (a : L) → ℝ)
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
have h : Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
  ((invariantExtension K L : (a : L) → ℝ) x : ℝ)
Tactic: rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pow hf_na hf_ext]
-- 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
inst_3 : IsUltrametricDist K
⊢ IsPowMul (spectralNorm K L)
have rw : IsPowMul (R := L) (⇑(invariantExtension K L) : (a : L) → ℝ)
Tactic: rw [spectralNorm_eq_invariantExtension K L]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst_3 : IsUltrametricDist K
⊢ spectralNorm K L 0 = 0
have rw : Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [spectralNorm_eq_invariantExtension K L, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst_3 : IsUltrametricDist K
rw : Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ spectralNorm K L 0 = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [spectralNorm_eq_invariantExtension K L, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst_3 : IsUltrametricDist K
⊢ ∀ (r s : L), spectralNorm K L (r + s) ≤ spectralNorm K L r + spectralNorm K L s
have rw : ∀ (r s : L),
  (invariantExtension K L : (a : L) → ℝ) (r + s) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)
      ((invariantExtension K L : (a : L) → ℝ) s : ℝ)
Tactic: rw [spectralNorm_eq_invariantExtension]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst_3 : IsUltrametricDist K
⊢ ∀ (r : L), spectralNorm K L (-r) = spectralNorm K L r
have rw : ∀ (r : L), Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) (-r) : ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)
Tactic: rw [spectralNorm_eq_invariantExtension]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst_3 : IsUltrametricDist K
⊢ ∀ (x y : L), spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y
have simp : ∀ (x y : L),
  (invariantExtension K L : (a : L) → ℝ) (x * y) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ)
      ((invariantExtension K L : (a : L) → ℝ) y : ℝ)
Tactic: simp only [spectralNorm_eq_invariantExtension]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst_3 : IsUltrametricDist K
x : L
⊢ spectralNorm K L x = 0 → x = 0
have simp : Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ) (0 : ℝ) → x = 0
Tactic: simp only [spectralNorm_eq_invariantExtension]
-- 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
inst_3 : IsUltrametricDist K
⊢ IsNonarchimedean (spectralNorm K L)
have rw : IsNonarchimedean (R := ℝ) (α := L) (⇑(invariantExtension K L) : (a : L) → ℝ)
Tactic: rw [spectralNorm_eq_invariantExtension]
-- 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
inst_3 : IsUltrametricDist K
x : K
⊢ spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
have rw : (invariantExtension K L : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
Tactic: rw [spectralNorm_eq_invariantExtension, invariantExtension_extends K L 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
inst_3 : IsUltrametricDist K
x : K
rw : (invariantExtension K L : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
⊢ spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
have rw₁ : ‖x‖ = ‖x‖
Tactic: rw [spectralNorm_eq_invariantExtension, invariantExtension_extends K L 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‖₊ : ℝ)
hf_iso :
  ∀ (σ : Gal(L/K)) (x : L), Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
x : L
⊢ Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)
have rw : Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)) (⨆ (x_1 : Gal(L/K)), (f : (a : L) → ℝ) x)
Tactic: rw [← @ciSup_const _ Gal(L/K) _ _ (f 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‖₊ : ℝ)
hf_iso :
  ∀ (σ : Gal(L/K)) (x : L), Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
x : L
σ : Gal(L/K)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)
have rw : Eq (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
Tactic: rw [hf_iso σ x]
-- 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‖₊ : ℝ)
hf_iso :
  ∀ (σ : Gal(L/K)) (x : L), Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
x : L
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have h_sup : Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)
Tactic: have h_sup : (⨆ σ : Gal(L/K), f (σ x)) = f x := by
    rw [← @ciSup_const _ Gal(L/K) _ _ (f x)]
    exact iSup_congr fun σ ↦ by rw [hf_iso σ 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‖₊ : ℝ)
hf_iso :
  ∀ (σ : Gal(L/K)) (x : L), Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
x : L
h_sup : Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have rw : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
Tactic: rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pm hf_na hf_ext, h_sup]
-- 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‖₊ : ℝ)
hf_iso :
  ∀ (σ : Gal(L/K)) (x : L), Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
x : L
h_sup : Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)
rw : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have rw₁ : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) x : ℝ)
Tactic: rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pm hf_na hf_ext, h_sup]
-- 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
k : K
⊢ spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) k : L) = ‖k‖
have simp_rw : spectralValue.{u_2} (R := K) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) k : K[X])) = ‖k‖
Tactic: simp_rw [spectralNorm, minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective]
-- 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
⊢ Eq.{u_3 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
have rw : Eq.{u_3 + 1} (α := L) 1 1
Tactic: rw [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
⊢ spectralNorm K L 1 = 1
have h1 : Eq.{u_3 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
Tactic: have h1 : (1 : L) = algebraMap K L 1 := by rw [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
h1 : Eq.{u_3 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
⊢ spectralNorm K L 1 = 1
have rw : spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) 1 : L) = 1
Tactic: rw [h1, spectralNorm_extends, norm_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
h1 : Eq.{u_3 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
rw : spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) 1 : L) = 1
⊢ spectralNorm K L 1 = 1
have rw₁ : Norm.norm.{u_2} (E := K) 1 = 1
Tactic: rw [h1, spectralNorm_extends, norm_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
h1 : Eq.{u_3 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)
rw : spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) 1 : L) = 1
rw₁ : Norm.norm.{u_2} (E := K) 1 = 1
⊢ spectralNorm K L 1 = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [h1, spectralNorm_extends, norm_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
inst_3 : IsUltrametricDist K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
⊢ spectralNorm K L (-y) = spectralNorm K L y
have h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
Tactic: haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional hy.isIntegral
-- 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
inst_3 : IsUltrametricDist K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
⊢ spectralNorm K L (-y) = spectralNorm K L y
have hy₁ : -y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (-g)
Tactic: have hy : -y = (algebraMap K⟮y⟯ L) (-g) := rfl
-- 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
inst_3 : IsUltrametricDist K
y : L
hy_1 : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (-g)
⊢ spectralNorm K L (-y) = spectralNorm K L y
have rw : (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
      (a : ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) → ℝ)
    (-(algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
            (a : ↥K⟮y⟯) → ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
          g :
      ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) =
  spectralNorm K ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))
    ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
          (a : ↥K⟮y⟯) → ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        g :
      ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
Tactic: rw [← spectralNorm.eq_of_normalClosure g (IntermediateField.AdjoinSimple.algebraMap_gen K y), hy,
    ← spectralNorm.eq_of_normalClosure (-g) hy, map_neg,
    ← spectralAlgNorm_of_finiteDimensional_normal_def]
-- 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
inst_3 : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
⊢ spectralNorm K L (k • y) = (↑‖k‖₊ : ℝ) * spectralNorm K L y
have h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
Tactic: haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional hy.isIntegral
-- 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
inst_3 : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
⊢ spectralNorm K L (k • y) = (↑‖k‖₊ : ℝ) * spectralNorm K L y
have hgy : k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)
Tactic: have hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g) := rfl