-- 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
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
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
by_cases hn : n = 0

Result:
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 (X ^ n - C a).Gal

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

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 (X ^ n - C a).Gal

Tactic:
rw [hn, pow_zero, ← C_1, ← C_sub]

Result:
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

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).Gal

Tactic:
exact gal_X_pow_isSolvable n

Result:
no goals

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
⊢ IsSolvable (X ^ n - C a).Gal

Tactic:
have ha' : algebraMap F (X ^ n - C a).SplittingField a ≠ 0 :=
  mt ((injective_iff_map_eq_zero _).mp (RingHom.injective _) a) ha

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
⊢ IsSolvable (X ^ n - C a).Gal

Proof state:
case 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 ^ 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
⊢ σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
rw [hc, mul_div_cancel₀ (σ b) hb']

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
⊢ (σ b / b) ^ n = 1

Tactic:
rw [div_pow, ← map_pow, hb, σ.commutes, div_self ha']

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
⊢ b ≠ 0

Tactic:
intro hb'

Result:
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
⊢ False

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 : 0 = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b = 0
⊢ False

Tactic:
exact ha' hb.symm

Result:
no goals

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

Tactic:
by_cases ha : a = 0

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 - C a).Gal

case neg
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

Proof state:
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 ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
⊢ (σ * τ) b = (τ * σ) b

Tactic:
have hb' : b ≠ 0 := by
  intro hb'
  rw [hb', zero_pow hn] at hb
  exact ha' hb.symm

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 ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
⊢ (σ * τ) b = (τ * σ) b

Proof state:
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

Tactic:
rw [σ.mul_apply, τ.mul_apply, hc, map_mul, τ.commutes, hd, map_mul, σ.commutes, hc,
  mul_assoc, mul_assoc, mul_right_inj' hb', mul_comm]

Result:
no goals