-- Mathlib/FieldTheory/AbelRuffini.lean
theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [Field F] {E : Type*} [Field E]
    (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : (X ^ n - C a).Splits i) :
    (X ^ n - 1 : F[X]).Splits i

Proof state:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
⊢ b ≠ 0

Tactic:
intro hb'

Result:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b = 0
⊢ False

Proof state:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
⊢ Splits i (X ^ n - 1)

Tactic:
have hs' : Multiset.card s = n := (natDegree_eq_card_roots h).symm.trans natDegree_X_pow_sub_C

Result:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
⊢ Splits i (X ^ n - 1)

Proof state:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = C (i a⁻¹) * (Polynomial.map i (X ^ n - C a)).comp (C b * X)
⊢ ((fun q => q.comp (C b * X)) ∘ fun c => X - C c) = fun c => C b * (X - C (c / b))

Tactic:
ext1 c

Result:
case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = C (i a⁻¹) * (Polynomial.map i (X ^ n - C a)).comp (C b * X)
c : E
⊢ ((fun q => q.comp (C b * X)) ∘ fun c => X - C c) c = C b * (X - C (c / b))

Proof state:
case pos
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : n = 0
⊢ Splits i 0

Tactic:
exact splits_zero i

Result:
no goals

Proof state:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
⊢ Splits i (X ^ n - 1)

Tactic:
apply @splits_of_exists_multiset F E _ _ i (X ^ n - 1) (s.map fun c : E => c / b)

Result:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
⊢ Polynomial.map i (X ^ n - 1) =
    C (i (X ^ n - 1).leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.map (fun c => c / b) s)).prod

Proof state:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ Splits i (X ^ n - 1)

Tactic:
have hn'' : (X ^ n - C a).degree ≠ 0 :=
  ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt WithBot.coe_eq_coe.mp hn)

Result:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
⊢ Splits i (X ^ n - 1)

Proof state:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
⊢ Polynomial.map i (X ^ n - 1) = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod

Tactic:
have key1 : (X ^ n - 1 : F[X]).map i = C (i a⁻¹) * ((X ^ n - C a).map i).comp (C b * X) := by
  rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
    Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
    mul_assoc, C_mul_C, one_mul]

Result:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : Polynomial.map i (X ^ n - 1) = C (i a⁻¹) * (Polynomial.map i (X ^ n - C a)).comp (C b * X)
⊢ Polynomial.map i (X ^ n - 1) = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod

Proof state:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
⊢ Splits i (X ^ n - 1)

Tactic:
obtain ⟨b, hb⟩ := exists_root_of_splits i h hn''

Result:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : eval₂ i b (X ^ n - C a) = 0
⊢ Splits i (X ^ n - 1)

Proof state:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = C (i (X ^ n - C a).leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ Splits i (X ^ n - 1)

Tactic:
rw [leadingCoeff_X_pow_sub_C hn', RingHom.map_one, C_1, one_mul] at hs

Result:
case neg.intro
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : Splits i (X ^ n - C a)
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots
hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod
⊢ Splits i (X ^ n - 1)