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
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
h : ∀ (x : L), spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x
⊢ spectralNorm K L = (⇑(invariantExtension K L) : (a : L) → ℝ)

Tactic:
ext 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
hu : IsUltrametricDist K
x : L
⊢ IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖

Tactic:
have hna := hu.isNonarchimedean_norm
-- 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
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean (R := ℝ) fun (x : K) ↦ ‖x‖
⊢ 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) → ℝ))
      ⋯;
  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) → ℝ))
      ⋯

Tactic:
set f := Classical.choose (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)
    with hf

Premises used: exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional, Classical.choose
-- 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
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) → ℝ))
      ⋯
⊢ 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
-- 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
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) → ℝ)
⊢ ∀ (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
-- 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
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‖
⊢ 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
-- 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
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) → ℝ)
h :
  Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
    ((invariantExtension K L : (a : L) → ℝ) x : ℝ)
⊢ spectralNorm K L x = (invariantExtension K L : (a : L) → ℝ) x

Tactic:
rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pow hf_na hf_ext]

Premises used: spectralNorm_eq_iSup_of_finiteDimensional_normal
-- 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
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) → ℝ)
⊢ Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
    ((invariantExtension K L : (a : L) → ℝ) x : ℝ)

Tactic:
simp only [invariantExtension_apply, algNormOfAlgEquiv_apply, hf]

Premises used: IsUltrametricDist.invariantExtension_apply, IsUltrametricDist.algNormOfAlgEquiv_apply
-- 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
inst_3 : IsUltrametricDist K
rw : IsPowMul (R := L) (⇑(invariantExtension K L) : (a : L) → ℝ)
⊢ IsPowMul (spectralNorm K L)

Tactic:
rw [spectralNorm_eq_invariantExtension K L]

Premises used: spectralNorm_eq_invariantExtension
-- 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
inst_3 : IsUltrametricDist K
⊢ IsPowMul (R := L) (⇑(invariantExtension K L) : (a : L) → ℝ)

Tactic:
isPowMul_invariantExtension K L

Premises used: IsUltrametricDist.isPowMul_invariantExtension
-- 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
inst_3 : IsUltrametricDist K
⊢ IsPowMul (R := L) (⇑(invariantExtension K L) : (a : L) → ℝ)

Tactic:
exact isPowMul_invariantExtension K L

Premises used: IsUltrametricDist.isPowMul_invariantExtension
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ spectralNorm K L 0 = 0

Tactic:
rw [spectralNorm_eq_invariantExtension K L, map_zero]

Premises used: spectralNorm_eq_invariantExtension, map_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 :
  ∀ (r s : L),
    (invariantExtension K L : (a : L) → ℝ) (r + s) ≤
      HAdd.hAdd (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)
        ((invariantExtension K L : (a : L) → ℝ) s : ℝ)
⊢ ∀ (r s : L), spectralNorm K L (r + s) ≤ spectralNorm K L r + spectralNorm K L s

Tactic:
rw [spectralNorm_eq_invariantExtension]

Premises used: spectralNorm_eq_invariantExtension
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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),
    (invariantExtension K L : (a : L) → ℝ) (r + s) ≤
      HAdd.hAdd (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)
        ((invariantExtension K L : (a : L) → ℝ) s : ℝ)

Tactic:
map_add_le_add _

Premises used: SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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),
    (invariantExtension K L : (a : L) → ℝ) (r + s) ≤
      HAdd.hAdd (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)
        ((invariantExtension K L : (a : L) → ℝ) s : ℝ)

Tactic:
exact map_add_le_add _

Premises used: SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 :
  ∀ (r : L),
    Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) (-r) : ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)
⊢ ∀ (r : L), spectralNorm K L (-r) = spectralNorm K L r

Tactic:
rw [spectralNorm_eq_invariantExtension]

Premises used: spectralNorm_eq_invariantExtension
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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),
    Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) (-r) : ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)

Tactic:
map_neg_eq_map _

Premises used: AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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),
    Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) (-r) : ℝ) ((invariantExtension K L : (a : L) → ℝ) r : ℝ)

Tactic:
exact map_neg_eq_map _

Premises used: AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
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 : ℝ)
⊢ ∀ (x y : L), spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
simp only [spectralNorm_eq_invariantExtension]

Premises used: spectralNorm_eq_invariantExtension
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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),
    (invariantExtension K L : (a : L) → ℝ) (x * y) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ)
        ((invariantExtension K L : (a : L) → ℝ) y : ℝ)

Tactic:
map_mul_le_mul (invariantExtension K L)

Premises used: IsUltrametricDist.invariantExtension, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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),
    (invariantExtension K L : (a : L) → ℝ) (x * y) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ)
        ((invariantExtension K L : (a : L) → ℝ) y : ℝ)

Tactic:
exact map_mul_le_mul (invariantExtension K L)

Premises used: IsUltrametricDist.invariantExtension, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
simp : Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ) (0 : ℝ) → x = 0
⊢ spectralNorm K L x = 0 → x = 0

Tactic:
simp only [spectralNorm_eq_invariantExtension]

Premises used: spectralNorm_eq_invariantExtension
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ) (0 : ℝ) → x = 0

Tactic:
eq_zero_of_map_eq_zero _

Premises used: AddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ) (0 : ℝ) → x = 0

Tactic:
exact eq_zero_of_map_eq_zero _

Premises used: AddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ ∀ (a : K) (x : L), spectralNorm K L (a • x) = ‖a‖ * spectralNorm K L x

Tactic:
simp [spectralNorm_eq_invariantExtension, AlgebraNormClass.map_smul_eq_mul _]

Premises used: AlgebraNormClass.map_smul_eq_mul, spectralNorm_eq_invariantExtension
-- 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
inst_3 : IsUltrametricDist K
x : L
⊢ (spectralAlgNorm_of_finiteDimensional_normal K L : (a : L) → ℝ) x = spectralNorm K L x

Tactic:
rfl

Premises used: iSup, spectralNorm, dite, spectralValue, rfl
-- 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
inst_3 : IsUltrametricDist K
rw : IsNonarchimedean (R := ℝ) (α := L) (⇑(invariantExtension K L) : (a : L) → ℝ)
⊢ IsNonarchimedean (spectralNorm K L)

Tactic:
rw [spectralNorm_eq_invariantExtension]

Premises used: spectralNorm_eq_invariantExtension
-- 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
inst_3 : IsUltrametricDist K
⊢ IsNonarchimedean (R := ℝ) (α := L) (⇑(invariantExtension K L) : (a : L) → ℝ)

Tactic:
isNonarchimedean_invariantExtension K L

Premises used: IsUltrametricDist.isNonarchimedean_invariantExtension
-- 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
inst_3 : IsUltrametricDist K
⊢ IsNonarchimedean (R := ℝ) (α := L) (⇑(invariantExtension K L) : (a : L) → ℝ)

Tactic:
exact isNonarchimedean_invariantExtension K L

Premises used: IsUltrametricDist.isNonarchimedean_invariantExtension
-- 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
inst_3 : IsUltrametricDist K
x : K
rw : (invariantExtension K L : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
rw₁ rw₂ : ‖x‖ = ‖x‖
⊢ spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) x : L) = ‖x‖

Tactic:
rw [spectralNorm_eq_invariantExtension, invariantExtension_extends K L x]

Premises used: IsUltrametricDist.invariantExtension_extends, spectralNorm_eq_invariantExtension
-- 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‖₊ : ℝ)
hf_iso :
  ∀ (σ : Gal(L/K)) (x : L), Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
x : L
rw :
  Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L)) (⨆ (x_1 : Gal(L/K)), (f : (a : L) → ℝ) x)
⊢ Eq (α := ℝ) (⨆ (σ : Gal(L/K)), (f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)

Tactic:
rw [← @ciSup_const _ Gal(L/K) _ _ (f x)]

Premises used: ciSup_const
-- 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‖₊ : ℝ)
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)
rw rw₁ : Eq (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) ((σ : (a : L) → L) x : L) : ℝ) ((f : (a : L) → ℝ) x : ℝ)

Tactic:
rw [hf_iso σ 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‖₊ : ℝ)
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)) (⨆ (x_1 : Gal(L/K)), (f : (a : L) → ℝ) x)

Tactic:
exact iSup_congr fun σ ↦ by rw [hf_iso σ x]

Premises used: iSup_congr
-- 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‖₊ : ℝ)
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 : ℝ)

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]
-- 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‖₊ : ℝ)
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) : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((f : (a : L) → ℝ) x : ℝ)
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x

Tactic:
rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pm hf_na hf_ext, h_sup]

Premises used: spectralNorm_eq_iSup_of_finiteDimensional_normal
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ SeminormClass.{u_3, u_2, u_3} (AlgebraNorm K ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))) K
    ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))

Tactic:
AlgebraNormClass.toSeminormClass

Premises used: AlgebraNormClass.toSeminormClass
-- 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
k : K
simp_rw : spectralValue.{u_2} (R := K) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) k : K[X])) = ‖k‖
⊢ spectralNorm.{u_2, u_3} K L ((algebraMap K L : (a : K) → L) k : L) = ‖k‖

Tactic:
simp_rw [spectralNorm, minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective]

Premises used: Algebra.algebraMap, minpoly.eq_X_sub_C_of_algebraMap_inj, spectralNorm, RingHom.injective
-- 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
k : K
⊢ spectralValue.{u_2} (R := K) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) k : K[X])) = ‖k‖

Tactic:
spectralValue_X_sub_C k

Premises used: spectralValue_X_sub_C