-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).Gal

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
⊢ ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m

Tactic:
intro σ

Result:
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ✝ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
σ : (X ^ n - 1).Gal
⊢ ∃ m, σ a = a ^ m

Proof state:
case neg.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ ∀ (a b : (X ^ n - 1).Gal), a * b = b * a

Tactic:
intro σ τ

Result:
case neg.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
⊢ σ * τ = τ * σ

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

Tactic:
by_cases hn : n = 0

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

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

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

Tactic:
have hn'' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1

Result:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ IsSolvable (X ^ n - 1).Gal

Proof state:
case intro
F : Type u_1
inst✝ : Field F
n : ℕ+
hn : ¬↑n = 0
hn'' : X ^ ↑n - 1 ≠ 0
σ✝ τ : (X ^ ↑n - 1).Gal
a : (X ^ ↑n - 1).SplittingField
ha : a ^ ↑n = 1
σ : (X ^ ↑n - 1).Gal
⊢ ∃ m, σ a = a ^ m

Tactic:
exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)

Result:
no goals

Proof state:
case neg.h.h.intro.intro
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ (σ * τ) a = (τ * σ) a

Tactic:
rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']

Result:
no goals

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

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

Result:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable (X ^ n - 1).Gal

Proof state:
case neg.h.h.intro
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
⊢ (σ * τ) a = (τ * σ) a

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

Result:
case neg.h.h.intro.intro
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ (σ * τ) a = (τ * σ) a

Proof state:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ IsSolvable (X ^ n - 1).Gal

Tactic:
apply isSolvable_of_comm

Result:
case neg.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
⊢ ∀ (a b : (X ^ n - 1).Gal), a * b = b * a

Proof state:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ∈ (X ^ n - 1).rootSet (X ^ n - 1).SplittingField
⊢ (σ * τ) a = (τ * σ) a

Tactic:
simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha

Result:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
⊢ (σ * τ) a = (τ * σ) a

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ✝ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
σ : (X ^ n - 1).Gal
⊢ ∃ m, σ a = a ^ m

Tactic:
lift n to ℕ+ using hn'

Result:
case intro
F : Type u_1
inst✝ : Field F
n : ℕ+
hn : ¬↑n = 0
hn'' : X ^ ↑n - 1 ≠ 0
σ✝ τ : (X ^ ↑n - 1).Gal
a : (X ^ ↑n - 1).SplittingField
ha : a ^ ↑n = 1
σ : (X ^ ↑n - 1).Gal
⊢ ∃ m, σ a = a ^ m

Proof state:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
⊢ (σ * τ) a = (τ * σ) a

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

Result:
case neg.h.h.intro
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
⊢ (σ * τ) a = (τ * σ) a

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

Tactic:
rw [hn, pow_zero, sub_self]

Result:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ IsSolvable (Gal 0)

Proof state:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
⊢ (σ * τ) a = (τ * σ) a

Tactic:
have key : ∀ σ : (X ^ n - 1 : F[X]).Gal, ∃ m : ℕ, σ a = a ^ m := by
  intro σ
  lift n to ℕ+ using hn'
  exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)

Result:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
⊢ (σ * τ) a = (τ * σ) a

Proof state:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ IsSolvable (Gal 0)

Tactic:
exact gal_zero_isSolvable

Result:
no goals

Proof state:
case neg.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
⊢ σ * τ = τ * σ

Tactic:
ext a ha

Result:
case neg.h.h
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ∈ (X ^ n - 1).rootSet (X ^ n - 1).SplittingField
⊢ (σ * τ) a = (τ * σ) a