-- Mathlib/FieldTheory/KummerExtension.lean
lemma isSplittingField_AdjoinRoot_X_pow_sub_C :
    haveI := Fact.mk H
    letI : Algebra K K[n√a] := inferInstance
    IsSplittingField K K[n√a] (X ^ n - C a)

Proof state:
case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a]) = ⊤

Tactic:
rw [eq_top_iff, ← AdjoinRoot.adjoinRoot_eq_top]

Result:
case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Algebra.adjoin K {root (X ^ n - C a)} ≤ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a])

Proof state:
case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Algebra.adjoin K {root (X ^ n - C a)} ≤ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a])

Tactic:
apply Algebra.adjoin_mono

Result:
case adjoin_rootSet'.H
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ {root (X ^ n - C a)} ⊆ (X ^ n - C a).rootSet K[n√a]

Proof state:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
w✝ : K
hζ : IsPrimitiveRoot w✝ n
⊢ Splits (RingHom.id K[n√a]) (X ^ n - C ((algebraMap K K[n√a]) a))

Tactic:
exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective)
  (root_X_pow_sub_C_pow n a)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ IsSplittingField K K[n√a] (X ^ n - C a)

Tactic:
constructor

Result:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Splits (algebraMap K K[n√a]) (X ^ n - C a)

case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a]) = ⊤

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
⊢ IsSplittingField K K[n√a] (X ^ n - C a)

Tactic:
have := Fact.mk H

Result:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this : Fact (Irreducible (X ^ n - C a))
⊢ IsSplittingField K K[n√a] (X ^ n - C a)

Proof state:
case adjoin_rootSet'.H
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ {root (X ^ n - C a)} ⊆ (X ^ n - C a).rootSet K[n√a]

Tactic:
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero
  (Nat.pos_of_ne_zero this) a), aeval_def, AdjoinRoot.algebraMap_eq, AdjoinRoot.eval₂_root]

Result:
no goals

Proof state:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Splits (algebraMap K K[n√a]) (X ^ n - 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
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Splits (RingHom.id K[n√a]) (X ^ n - C ((algebraMap K K[n√a]) a))

Proof state:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ Splits (RingHom.id K[n√a]) (X ^ n - C ((algebraMap K K[n√a]) a))

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

Result:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
w✝ : K
hζ : w✝ ∈ primitiveRoots n K
⊢ Splits (RingHom.id K[n√a]) (X ^ n - C ((algebraMap K K[n√a]) a))

Proof state:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
w✝ : K
hζ : w✝ ∈ primitiveRoots n K
⊢ Splits (RingHom.id K[n√a]) (X ^ n - C ((algebraMap K K[n√a]) a))

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero <| ne_zero_of_irreducible_X_pow_sub_C H)] at hζ

Result:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
w✝ : K
hζ : IsPrimitiveRoot w✝ n
⊢ Splits (RingHom.id K[n√a]) (X ^ n - C ((algebraMap K K[n√a]) a))

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this : Fact (Irreducible (X ^ n - C a))
⊢ IsSplittingField K K[n√a] (X ^ n - C a)

Tactic:
letI : Algebra K K[n√a] := inferInstance

Result:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ IsSplittingField K K[n√a] (X ^ n - C a)

Proof state:
case adjoin_rootSet'.H
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ {root (X ^ n - C a)} ⊆ (X ^ n - C a).rootSet K[n√a]

Tactic:
have := ne_zero_of_irreducible_X_pow_sub_C H

Result:
case adjoin_rootSet'.H
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ {root (X ^ n - C a)} ⊆ (X ^ n - C a).rootSet K[n√a]