-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_pow_sub_C_isSolvable (n : ℕ) (x : F) : IsSolvable (X ^ n - C x).Gal

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
⊢ IsSolvable (X ^ n - C x).Gal

Tactic:
by_cases hx : x = 0

Result:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable (X ^ n - C x).Gal

case neg
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (X ^ n - C x).Gal

Proof state:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable (X ^ n).Gal

Tactic:
exact gal_X_pow_isSolvable n

Result:
no goals

Proof state:
case neg.hpq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (algebraMap F (X ^ n - C x).SplittingField) (X ^ n - 1)

Tactic:
exact splits_X_pow_sub_one_of_X_pow_sub_C _ n hx (SplittingField.splits _)

Result:
no goals

Proof state:
case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (X ^ n - 1).Gal

Tactic:
exact gal_X_pow_sub_one_isSolvable n

Result:
no goals

Proof state:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (X ^ n - C ((algebraMap F (X ^ n - 1).SplittingField) x)).Gal

Tactic:
apply gal_X_pow_sub_C_isSolvable_aux

Result:
case neg.hq.h
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (RingHom.id (X ^ n - 1).SplittingField) (X ^ n - 1)

Proof state:
case neg.hq.h
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (RingHom.id (X ^ n - 1).SplittingField) (X ^ n - 1)

Tactic:
have key := SplittingField.splits (X ^ n - 1 : F[X])

Result:
case neg.hq.h
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
key : Splits (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - 1)
⊢ Splits (RingHom.id (X ^ n - 1).SplittingField) (X ^ n - 1)

Proof state:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (X ^ n - C x).Gal

Tactic:
apply gal_isSolvable_tower (X ^ n - 1) (X ^ n - C x)

Result:
case neg.hpq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (algebraMap F (X ^ n - C x).SplittingField) (X ^ n - 1)

case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (X ^ n - 1).Gal

case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (Polynomial.map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

Proof state:
case neg.hq.h
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
key : Splits (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - 1)
⊢ Splits (RingHom.id (X ^ n - 1).SplittingField) (X ^ n - 1)

Tactic:
rwa [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, map_X,
  Polynomial.map_one] at key

Result:
no goals

Proof state:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (Polynomial.map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

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

Result:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable (X ^ n - C ((algebraMap F (X ^ n - 1).SplittingField) x)).Gal

Proof state:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable (X ^ n - C x).Gal

Tactic:
rw [hx, C_0, sub_zero]

Result:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable (X ^ n).Gal