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
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⟯)))
have 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⟯)))
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]
-- 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
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⟯)))
⊢ (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⟯)))
have 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
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]
-- 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
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
⊢ (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⟯)))
have 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
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]
-- 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
hgy : k • y = (algebraMap (↥K⟮y⟯) L : (a : ↥K⟮y⟯) → L) (k • g)
⊢ spectralNorm K L (k • y) = (↑‖k‖₊ : ℝ) * spectralNorm K L y
have 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⟯)))
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]
-- 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
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⟯)))
⊢ spectralNorm K L (k • y) = (↑‖k‖₊ : ℝ) * spectralNorm K L y
have 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⟯)))
Tactic: rw [← spectralNorm.eq_of_normalClosure g (IntermediateField.AdjoinSimple.algebraMap_gen K y), hgy,
    ← spectralNorm.eq_of_normalClosure (k • g) rfl, h]
-- 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
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y
have h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
Tactic: haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.finiteDimensional_adjoin_pair hx.isIntegral 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
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
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y
have hxy : 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
-- 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
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)
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y
have 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⟯)))
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]
-- 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
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n
have h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
Tactic: haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional (h_alg.isAlgebraic x).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
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
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n
have hg : let g : ↥K⟮x⟯ := AdjoinSimple.gen K x;
g = AdjoinSimple.gen K x
Tactic: set g := IntermediateField.AdjoinSimple.gen K x with hg
-- 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
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
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n
have h_map : 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
-- 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
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
h_map : HPow.hPow (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) g : L) n = x ^ n
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n
have rw : spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
    (HPow.hPow (α := ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
      ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
            (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
          g :
        ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
      n) =
  spectralNorm K ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))
      ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
            (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
          g :
        ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) ^
    n
Tactic: rw [← spectralNorm.eq_of_normalClosure _ (IntermediateField.AdjoinSimple.algebraMap_gen K x),
    ← spectralNorm.eq_of_normalClosure (g ^ n) h_map, map_pow, ← hg]
-- 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
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)
have h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
Tactic: haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.finiteDimensional_adjoin_pair (h_alg.isAlgebraic x).isIntegral
       (h_alg.isAlgebraic y).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
h_alg : Algebra.IsAlgebraic K L
x y : L
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
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)
have hxy : 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
-- 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
h_alg : Algebra.IsAlgebraic K L
x y : L
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)
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)
have rw : spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
    (HAdd.hAdd (α := ↥(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⟯)))) ≤
  max
    (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: 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),
    _root_.map_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
⊢ ((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) (k • x) =
    HMul.hMul (β := ℝ) ‖k‖
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ)
have rw : HMul.hMul (α := ℝ) (β := ℝ)
    (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
        ((algebraMap K L : (a : K) → L) k : L) :
      ℝ)
    (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ) =
  HMul.hMul (β := ℝ) ‖k‖
    (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ)
Tactic: rw [Algebra.smul_def, map_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
⊢ HMul.hMul (α := ℝ) (β := ℝ)
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
          ((algebraMap K L : (a : K) → L) k : L) :
        ℝ)
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ) =
    HMul.hMul (β := ℝ) ‖k‖
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ)
have e_a : ((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
    ((algebraMap K L : (a : K) → L) k : L) =
  ‖k‖
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
⊢ ((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) k : L) =
    ‖k‖
have e_a : Eq (α := ℝ)
  (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) k : L) :
    ℝ)
  ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
Tactic: rw [← hf_ext k]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
g : AlgebraNorm K L :=
  let __src := Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f;
  { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have hg_pow : IsPowMul (R := L) (⇑g : (a : L) → ℝ)
Tactic: have hg_pow : IsPowMul g := MulRingNorm.isPowMul _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
g : AlgebraNorm K L :=
  let __src := Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f;
  { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }
hg_pow : IsPowMul (R := L) (⇑g : (a : L) → ℝ)
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have hgx : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((g : (a : L) → ℝ) x : ℝ)
Tactic: have hgx : f x = g x := rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
g : AlgebraNorm K L :=
  let __src := Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f;
  { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }
hg_pow : IsPowMul (R := L) (⇑g : (a : L) → ℝ)
hgx : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((g : (a : L) → ℝ) x : ℝ)
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have rw : (g : (a : L) → ℝ) x = spectralNorm K L x
Tactic: rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
g : AlgebraNorm K L :=
  let __src := Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f;
  { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }
hg_pow : IsPowMul (R := L) (⇑g : (a : L) → ℝ)
hgx : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((g : (a : L) → ℝ) x : ℝ)
rw : (g : (a : L) → ℝ) x = spectralNorm K L x
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have rw₁ : (spectralAlgNorm K L : (a : L) → ℝ) x = spectralNorm K L x
Tactic: rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]