-- Mathlib/FieldTheory/KummerExtension.lean
lemma isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top
    {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a) (hα : K⟮α⟯ = ⊤) :
    IsSplittingField K L (X ^ (finrank K L) - C a)

Proof state:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
w✝ : K
hζ : w✝ ∈ primitiveRoots (finrank K L) K
⊢ Splits (RingHom.id L) (X ^ finrank K L - C ((algebraMap K L) a))

Tactic:
rw [mem_primitiveRoots finrank_pos] at hζ

Result:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
w✝ : K
hζ : IsPrimitiveRoot w✝ (finrank K L)
⊢ Splits (RingHom.id L) (X ^ finrank K L - C ((algebraMap K L) a))

Proof state:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Splits (algebraMap K L) (X ^ finrank K L - C a)

Tactic:
rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C,
  Polynomial.map_X]

Result:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Splits (RingHom.id L) (X ^ finrank K L - C ((algebraMap K L) a))

Proof state:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Splits (RingHom.id L) (X ^ finrank K L - C ((algebraMap K L) a))

Tactic:
have ⟨_, hζ⟩ := hK

Result:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
w✝ : K
hζ : w✝ ∈ primitiveRoots (finrank K L) K
⊢ Splits (RingHom.id L) (X ^ finrank K L - C ((algebraMap K L) a))

Proof state:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L) = ⊤

Tactic:
rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
  IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite K α)]

Result:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Algebra.adjoin K {α} ≤ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L)

Proof state:
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ IsSplittingField K L (X ^ finrank K L - C a)

Tactic:
constructor

Result:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Splits (algebraMap K L) (X ^ finrank K L - C a)

case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L) = ⊤

Proof state:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Algebra.adjoin K {α} ≤ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L)

Tactic:
apply Algebra.adjoin_mono

Result:
case adjoin_rootSet'.H
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ {α} ⊆ (X ^ finrank K L - C a).rootSet L

Proof state:
case adjoin_rootSet'.H
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ {α} ⊆ (X ^ finrank K L - C a).rootSet L

Tactic:
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
  aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]

Result:
no goals

Proof state:
case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
w✝ : K
hζ : IsPrimitiveRoot w✝ (finrank K L)
⊢ Splits (RingHom.id L) (X ^ finrank K L - C ((algebraMap K L) a))

Tactic:
exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha

Result:
no goals