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
k : K
⊢ spectralValue.{u_2} (R := K) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) k : K[X])) = ‖k‖

Tactic:
exact spectralValue_X_sub_C k

Premises used: spectralValue_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
rw rw₁ : Eq.{u_3 + 1} (α := L) 1 1
⊢ Eq.{u_3 + 1} (α := L) (1 : L) ((algebraMap K L : (a : K) → L) 1 : L)

Tactic:
rw [map_one]

Premises used: 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
⊢ 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]
-- 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
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
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ spectralNorm K L 1 = 1

Tactic:
rw [h1, spectralNorm_extends, norm_one]

Premises used: NormOneClass.norm_one, spectralNorm_extends
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
⊢ FiniteDimensional.{u_2, u_3} K ↥E

Tactic:
haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional hy.isIntegral
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ -y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (-g)

Tactic:
have hy : -y = (algebraMap K⟮y⟯ L) (-g) := 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
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)
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⟯)))
⊢ spectralNorm K L (-y) = spectralNorm K L 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]

Premises used: map_neg, spectralNorm.eq_of_normalClosure, spectralAlgNorm_of_finiteDimensional_normal_def, Neg.neg, IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : 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)
⊢ (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:
map_neg_eq_map _ _

Premises used: iSup, AddGroupSeminormClass.map_neg_eq_map, spectralNorm, dite, 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
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)
⊢ (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:
exact map_neg_eq_map _ _

Premises used: AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
⊢ FiniteDimensional.{u_2, u_3} K ↥E

Tactic:
haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional hy.isIntegral
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
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
⊢ k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)

Tactic:
have hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g) := 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
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
hgy : k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)
rw :
  HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) 1 =
    HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
      ((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⟯)))
rw₁ :
  HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) 1 =
    k • HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g 1
rw₂ rw₃ :
  k • HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g 1 =
    k • HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g 1
⊢ (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
        (a : ↥K⟮y⟯) → ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • g) =
    HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
      ((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 [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]

Premises used: smul_assoc, Algebra.algebraMap_eq_smul_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
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
hgy : k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)
⊢ (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
        (a : ↥K⟮y⟯) → ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • g) =
    HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
      ((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:
have h : algebraMap K⟮y⟯ (normalClosure K K⟮y⟯ (AlgebraicClosure K⟮y⟯)) (k • g) =
      k • algebraMap K⟮y⟯ (normalClosure K K⟮y⟯ (AlgebraicClosure K⟮y⟯)) g := by
    rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : 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
hgy : k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
        (a : ↥K⟮y⟯) → ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • g) =
    HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
      ((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⟯)))
rw :
  spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
        ((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⟯)))) =
    (↑‖k‖₊ : ℝ) *
      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⟯)))
⊢ spectralNorm K L (k • y) = (↑‖k‖₊ : ℝ) * spectralNorm K L y

Tactic:
rw [← spectralNorm.eq_of_normalClosure g (IntermediateField.AdjoinSimple.algebraMap_gen K y), hgy,
    ← spectralNorm.eq_of_normalClosure (k • g) rfl, h]

Premises used: spectralNorm.eq_of_normalClosure, HSMul.hSMul, rfl, IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : 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
hgy : k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
        (a : ↥K⟮y⟯) → ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • g) =
    HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
      ((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⟯)))
⊢ (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)) :
        (a : ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) → ℝ)
      (HSMul.hSMul (β := ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) k
        ((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⟯)))) =
    (↑‖k‖₊ : ℝ) *
      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:
apply map_smul_eq_mul

Premises used: SeminormClass.map_smul_eq_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
inst_3 : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
⊢ FiniteDimensional.{u_2, u_3} K ↥E

Tactic:
haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.finiteDimensional_adjoin_pair hx.isIntegral hy.isIntegral
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
⊢ x * y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx * gy)

Tactic:
have hxy : x * y = (algebraMap K⟮x, y⟯ L) (gx * gy) := 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
inst_3 : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx * gy)
rw :
  (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
        (a : ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) → ℝ)
      (HMul.hMul (α := ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (β :=
        ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))) ≤
    spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) *
      spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
rw [hxy, ← spectralNorm.eq_of_normalClosure (gx * gy) hxy,
    ← spectralNorm.eq_of_normalClosure gx (IntermediateField.AdjoinPair.algebraMap_gen₁ K x y),
    ← spectralNorm.eq_of_normalClosure gy (IntermediateField.AdjoinPair.algebraMap_gen₂ K x y),
    map_mul, ← spectralAlgNorm_of_finiteDimensional_normal_def]

Premises used: HMul.hMul, map_mul, IntermediateField.AdjoinPair.algebraMap_gen₁, spectralNorm.eq_of_normalClosure, spectralAlgNorm_of_finiteDimensional_normal_def, IntermediateField.AdjoinPair.algebraMap_gen₂
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx * gy)
⊢ (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
        (a : ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) → ℝ)
      (HMul.hMul (α := ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (β :=
        ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))) ≤
    spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) *
      spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))

Tactic:
map_mul_le_mul _ _ _

Premises used: iSup, spectralNorm, dite, spectralValue, SubmultiplicativeHomClass.map_mul_le_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
inst_3 : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx * gy)
⊢ (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
        (a : ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) → ℝ)
      (HMul.hMul (α := ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (β :=
        ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))) ≤
    spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) *
      spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))

Tactic:
exact map_mul_le_mul _ _ _

Premises used: SubmultiplicativeHomClass.map_mul_le_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
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
⊢ FiniteDimensional.{u_2, u_3} K ↥E

Tactic:
haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional (h_alg.isAlgebraic x).isIntegral
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
⊢ let g : ↥K⟮x⟯ := AdjoinSimple.gen K x;
  g = AdjoinSimple.gen K x

Tactic:
set g := IntermediateField.AdjoinSimple.gen K x with hg

Premises used: IntermediateField.AdjoinSimple.gen
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
⊢ HPow.hPow (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) g : L) n = x ^ n

Tactic:
have h_map : algebraMap E L g ^ n = x ^ n := rfl