-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
    (h : (X ^ n - 1 : F[X]).Splits (RingHom.id F)) : IsSolvable (X ^ n - C a).Gal

Proof state:
case neg.h
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
⊢ σ * τ = τ * σ

Tactic:
ext b hb

Result:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ∈ (X ^ n - C a).rootSet (X ^ n - C a).SplittingField
⊢ (σ * τ) b = (τ * σ) b

Proof state:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
have hn' : 0 < n := pos_iff_ne_zero.mpr hn

Result:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable (X ^ n - C a).Gal

Proof state:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : n = 0
⊢ IsSolvable (C (1 - a)).Gal

Tactic:
exact gal_C_isSolvable (1 - a)

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
key : (σ b / b) ^ n = 1
⊢ ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
obtain ⟨c, hc⟩ := mem_range key

Result:
case intro
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
key : (σ b / b) ^ n = 1
c : F
hc : (algebraMap F (X ^ n - C a).SplittingField) c = σ b / b
⊢ ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Proof state:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a

Result:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
⊢ IsSolvable (X ^ n - C a).Gal

Proof state:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
apply isSolvable_of_comm

Result:
case neg.h
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
⊢ ∀ (a_1 b : (X ^ n - C a).Gal), a_1 * b = b * a_1

Proof state:
case neg.h.h.intro
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
⊢ (σ * τ) b = (τ * σ) b

Tactic:
obtain ⟨d, hd⟩ := key τ

Result:
case neg.h.h.intro.intro
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ (σ * τ) b = (τ * σ) b

Proof state:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : a = 0
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
rw [ha, C_0, sub_zero]

Result:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : a = 0
⊢ IsSolvable (X ^ n).Gal

Proof state:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
have mem_range : ∀ {c : (X ^ n - C a).SplittingField},
    (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) := fun {c} hc =>
  RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (h.def.resolve_left hn'''
    (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))
    (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one]))))

Result:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
⊢ IsSolvable (X ^ n - C a).Gal