awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
⊢ ‖x_2 • x_3‖ ≤ ‖x_2‖ * ‖x_3‖
have hab : ‖x_2 • x_3‖ = ‖x_2‖ * ‖x_3‖
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
⊢ ‖x_2 • x_3‖ = ‖x_2‖ * ‖x_3‖
have hab : norm.{u_3} (E := L) ((algebraMap E L : (a : E) → L) x_2 : L) = ‖x_2‖ ∨ x_3 = 0
Tactic: simp only [Algebra.smul_def, norm_mul, mul_eq_mul_right_iff, _root_.norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
⊢ norm.{u_3} (E := L) ((algebraMap E L : (a : E) → L) x_2 : L) = ‖x_2‖ ∨ x_3 = 0
have hab : spectralNorm.{u, u_3} K L ((algebraMap E L : (a : E) → L) x_2 : L) = spectralNorm K E x_2 ∨ x_3 = 0
Tactic: simp only [NormedAlgebra.norm_eq_spectralNorm 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
have ha₁ : Ne.{u_2 + 1} (α := E[X]) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x) : E[X])
    (0 : E[X]) ∧
  eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) = 0
Tactic: simp only [mem_roots', IsRoot.def] at ha
Cleared hypotheses: ha
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Ne.{u_2 + 1} (α := E[X]) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x) : E[X])
      (0 : E[X]) ∧
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) = 0
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
have rw : (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
  eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
Tactic: rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Ne.{u_2 + 1} (α := E[X]) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x) : E[X])
      (0 : E[X]) ∧
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) = 0
rw :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
have rw₁ : (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
  eval a (Polynomial.map (algebraMap K E) (minpoly K x))
Tactic: rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Ne.{u_2 + 1} (α := E[X]) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x) : E[X])
      (0 : E[X]) ∧
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) = 0
rw :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
rw₁ :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (Polynomial.map (algebraMap K E) (minpoly K x))
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
have rw₂ : (aeval a : (a : K[X]) → E) (minpoly K x) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))
Tactic: rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Ne.{u_2 + 1} (α := E[X]) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x) : E[X])
      (0 : E[X]) ∧
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) = 0
rw :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
rw₁ :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (Polynomial.map (algebraMap K E) (minpoly K x))
rw₂ : (aeval a : (a : K[X]) → E) (minpoly K x) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
have rw₃ : eval₂ (algebraMap K E) a (minpoly K x) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))
Tactic: rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Ne.{u_2 + 1} (α := E[X]) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x) : E[X])
      (0 : E[X]) ∧
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) = 0
rw :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
rw₁ :
  (aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) =
    eval a (Polynomial.map (algebraMap K E) (minpoly K x))
rw₂ : (aeval a : (a : K[X]) → E) (minpoly K x) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))
rw₃ : eval₂ (algebraMap K E) a (minpoly K x) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
have rw₄ : eval₂ (algebraMap K E) a (minpoly K x) = eval₂ (algebraMap K E) a (minpoly K x)
Tactic: rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a
⊢ spectralValue.{u} (R := K) (minpoly K a) =
    spectralValue.{u} (R := K) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E))
have this : Eq.{u_2 + 1} (α := E)
  ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
Tactic: have : (aeval a) (minpoly K ((algebraMap L E) x)) = 0 := by
    simp only [mem_roots', IsRoot.def] at ha
    rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : Algebra.IsAlgebraic K E
a : E
ha :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a
this :
  Eq.{u_2 + 1} (α := E)
    ((aeval a : (a : K[X]) → E) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E)) : E) (0 : E)
⊢ spectralValue.{u} (R := K) (minpoly K a) =
    spectralValue.{u} (R := K) (minpoly.{u, u_2} K (B := E) ((algebraMap L E : (a : L) → E) x : E))
have rw : spectralValue.{u} (R := K) (minpoly K a) = spectralValue.{u} (R := K) (minpoly K a)
Tactic: rw [← minpoly.eq_of_root (Algebra.IsAlgebraic.isAlgebraic ((algebraMap L E) x)) this]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
⊢ natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
have trans : natDegree (minpoly K x) =
  natDegree.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
Tactic: trans (mapAlg K E (minpoly K x)).natDegree
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
trans :
  natDegree (minpoly K x) =
    natDegree.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
⊢ natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
have trans₁ : natDegree.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) =
  Multiset.card.{u_2} (α := E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
Tactic: trans (mapAlg K E (minpoly K x)).natDegree
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
⊢ natDegree (minpoly K x) =
    natDegree.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
have rw : natDegree (minpoly K x) = natDegree (Polynomial.map (algebraMap K E) (minpoly K x))
Tactic: rw [mapAlg_eq_map, natDegree_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
rw : natDegree (minpoly K x) = natDegree (Polynomial.map (algebraMap K E) (minpoly K x))
⊢ natDegree (minpoly K x) =
    natDegree.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
have rw₁ : natDegree (minpoly K x) = natDegree (minpoly K x)
Tactic: rw [mapAlg_eq_map, natDegree_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
⊢ natDegree.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
have rw : Splits.{u_2} (R := E) (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
Tactic: rw [eq_comm, ← splits_iff_card_roots]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
⊢ HPow.hPow (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
      (natDegree (minpoly K x)) =
    (spectralMulAlgNorm K E : (a : E) → ℝ)
      (Multiset.prod (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have h_deg : natDegree (minpoly K x) =
  Multiset.card.{u_2} (α := E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
Tactic: have h_deg : (minpoly K x).natDegree = Multiset.card ((mapAlg K E) (minpoly K x)).roots := by
    trans (mapAlg K E (minpoly K x)).natDegree
    · rw [mapAlg_eq_map, natDegree_map]
    · rw [eq_comm, ← splits_iff_card_roots]
      exact IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
⊢ HPow.hPow (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
      (natDegree (minpoly K x)) =
    (spectralMulAlgNorm K E : (a : E) → ℝ)
      (Multiset.prod (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have rw : Eq (α := ℝ)
  (Multiset.prod
      (Multiset.replicate (natDegree (minpoly K x))
        ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E))) :
    ℝ)
  (Multiset.prod
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))) :
    ℝ)
Tactic: rw [map_multiset_prod, ← Multiset.prod_replicate]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
⊢ Eq (α := ℝ)
    (Multiset.prod
        (Multiset.replicate (natDegree (minpoly K x))
          ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E))) :
      ℝ)
    (Multiset.prod
        (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
          (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))) :
      ℝ)
have h : Eq (α := Multiset ℝ)
  (Multiset.replicate (natDegree (minpoly K x))
      ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E)) :
    Multiset ℝ)
  (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) :
    Multiset ℝ)
Tactic: apply congr_arg
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
⊢ Eq (α := Multiset ℝ)
    (Multiset.replicate (natDegree (minpoly K x))
        ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E)) :
      Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) :
      Multiset ℝ)
have h : ∀ (r : ℝ),
  Multiset.count r
      (Multiset.replicate (natDegree (minpoly K x))
        ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E))) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
Tactic: ext r
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
⊢ Multiset.count r
      (Multiset.replicate (natDegree (minpoly K x))
        ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E))) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have h : (if (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r then natDegree (minpoly K x)
  else 0) =
  Multiset.count r
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
Tactic: rw [Multiset.count_replicate]