awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
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
h_fin : FiniteDimensional K L
this_1 : NormedAddCommGroup L := normedAddCommGroup K L
this : NormedSpace K L := normedSpace K L
⊢ CompleteSpace L

Tactic:
FiniteDimensional.complete K L

Premises used: FiniteDimensional.complete
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
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
h_fin : FiniteDimensional K L
this_1 : NormedAddCommGroup L := normedAddCommGroup K L
this : NormedSpace K L := normedSpace K L
⊢ CompleteSpace L

Tactic:
exact FiniteDimensional.complete K L

Premises used: FiniteDimensional.complete
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ 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

Premises used: Polynomial.IsRoot.def, Polynomial.mem_roots'
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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))
rw₄ rw₅ : eval₂ (algebraMap K E) a (minpoly K x) = eval₂ (algebraMap K E) a (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)

Tactic:
rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]

Premises used: Polynomial.eval_map, Algebra.algebraMap, Polynomial.mapAlg_eq_map, Polynomial.aeval_def, RingHom.injective, And.right, minpoly.algebraMap_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)

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]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)
rw rw₁ : spectralValue.{u} (R := K) (minpoly K a) = spectralValue.{u} (R := K) (minpoly K 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))

Tactic:
rw [← minpoly.eq_of_root (Algebra.IsAlgebraic.isAlgebraic ((algebraMap L E) x)) this]

Premises used: Algebra.IsAlgebraic.isAlgebraic, Algebra.algebraMap, minpoly.eq_of_root, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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))
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)))
⊢ 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:
trans (mapAlg K E (minpoly K x)).natDegree

Premises used: minpoly, Polynomial.mapAlg, Polynomial.natDegree, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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))
rw₁ rw₂ : natDegree (minpoly K x) = natDegree (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))

Tactic:
rw [mapAlg_eq_map, natDegree_map]

Premises used: Polynomial.natDegree_map, Polynomial.mapAlg_eq_map
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : 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))
⊢ 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:
rw [eq_comm, ← splits_iff_card_roots]

Premises used: eq_comm, Polynomial.splits_iff_card_roots
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ 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:
IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)

Premises used: minpoly, Polynomial.IsSplittingField.IsScalarTower.splits
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ 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:
exact IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)

Premises used: minpoly, Polynomial.IsSplittingField.IsScalarTower.splits
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)))

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)
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)))
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)))) :
      ℝ)
⊢ 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))))

Tactic:
rw [map_multiset_prod, ← Multiset.prod_replicate]

Premises used: Multiset.prod_replicate, map_multiset_prod
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)))
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 ℝ)
⊢ 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:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)))
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))))
⊢ 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:
ext r
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ
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))))
⊢ 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:
rw [Multiset.count_replicate]

Premises used: Multiset.count_replicate
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ
pos :
  ∀ (hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r),
    natDegree (minpoly K x) =
      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))))
neg :
  ∀ (hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r),
    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))))
⊢ (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:
split_ifs with hr
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
s : ℝ
hs :
  Membership.mem (γ := 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))))
    s
obtain :
  ∀ (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)
    (has : (spectralMulAlgNorm K E : (a : E) → ℝ) a = s), r = s
⊢ r = s

Tactic:
obtain ⟨a, ha, has⟩ := Multiset.mem_map.mp hs

Premises used: Multiset.mem_map, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
s : ℝ
hs :
  Membership.mem (γ := 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))))
    s
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
has : (spectralMulAlgNorm K E : (a : E) → ℝ) a = s
rw : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = s
rw₁ :
  Eq (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
    ((spectralMulAlgNorm K E : (a : E) → ℝ) a : ℝ)
rw₂ rw₃ :
  Eq (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
    ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
⊢ r = s

Tactic:
rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]

Premises used: spectralNorm.spectralMulAlgNorm_eq_of_mem_roots
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
⊢ ∀ (s : ℝ),
    Membership.mem (γ := 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))))
        s →
      r = s

Tactic:
have h : ∀ s ∈ Multiset.map (spectralMulAlgNorm K E) ((mapAlg K E) (minpoly K x)).roots,
        r = s := by
      intro s hs
      obtain ⟨a, ha, has⟩ := Multiset.mem_map.mp hs
      rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
h :
  ∀ (s : ℝ),
    Membership.mem (γ := 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))))
        s →
      r = s
pos :
  natDegree (minpoly K x) =
    Multiset.card (α := ℝ)
      (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))))
pos₁ pos₂ pos₃ pos₄ :
  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)))
⊢ natDegree (minpoly K x) =
    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:
rwa [Multiset.count_eq_card.mpr h, Multiset.card_map]

Premises used: Iff.mpr, Multiset.count_eq_card, Multiset.card_map