awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
⊢ s.card = n

Tactic:
have hs' : Multiset.card s = n := by
    rw [← h.natDegree_eq_card_roots, natDegree_map, natDegree_X_pow_sub_C]
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
neg :
  ∃ (m : Multiset E),
    map i (HPow.hPow (α := F[X]) X n - 1) =
      HMul.hMul (α := E[X]) (β := E[X])
        ((C : (a : E) → E[X]) ((i : (a : F) → E) (HPow.hPow (α := F[X]) X n - 1).leadingCoeff) : E[X])
        (Multiset.prod
            (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) m) :
          E[X])
⊢ (map i (HPow.hPow (α := F[X]) X n - 1)).Splits

Tactic:
rw [splits_iff_exists_multiset, leadingCoeff_map]

Premises used: Polynomial.splits_iff_exists_multiset, Polynomial.leadingCoeff_map
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
h₁ :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) (β := E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) (HPow.hPow (α := F[X]) X n - 1).leadingCoeff) : E[X])
      (Multiset.prod
          (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]))
            (Multiset.map (fun (c : E) ↦ c / b) s)) :
        E[X])
⊢ ∃ (m : Multiset E),
    map i (HPow.hPow (α := F[X]) X n - 1) =
      HMul.hMul (α := E[X]) (β := E[X])
        ((C : (a : E) → E[X]) ((i : (a : F) → E) (HPow.hPow (α := F[X]) X n - 1).leadingCoeff) : E[X])
        (Multiset.prod
            (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) m) :
          E[X])

Tactic:
use (s.map fun c ↦ c / b)

Premises used: Multiset.map, HDiv.hDiv
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
h₁ :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    Multiset.prod
      (Multiset.map
        ((fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) ∘ fun (c : E) ↦ c / b) s)
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) (β := E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) (HPow.hPow (α := F[X]) X n - 1).leadingCoeff) : E[X])
      (Multiset.prod
          (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]))
            (Multiset.map (fun (c : E) ↦ c / b) s)) :
        E[X])

Tactic:
rw [leadingCoeff_X_pow_sub_one hn', map_one, C_1, one_mul, Multiset.map_map]

Premises used: Polynomial.C_1, map_one, Multiset.map_map, Polynomial.leadingCoeff_X_pow_sub_one, one_mul
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
rw :
  Eq (α := E[X])
    ((C : (a : E) → E[X]) (HMul.hMul (α := E) (β := E) ((i : (a : F) → E) a⁻¹ : E) ((i : (a : F) → E) a : E)) : E[X])
    (1 : E[X])
rw₁ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) (a⁻¹ * a)) : E[X]) (1 : E[X])
rw₂ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) 1)) 1
rw₃ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) 1) 1
rw₄ rw₅ : Eq.{u_4 + 1} (α := E[X]) 1 1
⊢ HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1

Tactic:
rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]

Premises used: Polynomial.C_1, RingHom.map_one, Polynomial.C_mul, RingHom.map_mul, inv_mul_cancel₀
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
⊢ HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1

Tactic:
have C_mul_C : C (i a⁻¹) * C (i a) = 1 := by
    rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))

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]
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
key1 :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
h₁ :
  ∀ (c : E),
    ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
          HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
        c =
      HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
        (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
⊢ Eq.{u_4 + 1} (α := E → E[X])
    ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
    fun (c : E) ↦
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))

Tactic:
ext1 c
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
key1 :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
⊢ Eq.{u_4 + 1} (α := E → E[X])
    ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
    fun (c : E) ↦
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))

Tactic:
have key2 : ((fun q : E[X] => q.comp (C b * X)) ∘ fun c : E => X - C c) = fun c : E =>
      C b * (X - C (c / b)) := by
    ext1 c
    dsimp only [Function.comp_apply]
    rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
key1 :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
key2 :
  Eq.{u_4 + 1} (α := E → E[X])
    ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
    fun (c : E) ↦
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
h₁ :
  Eq (α := E[X])
    (Multiset.prod
      (Multiset.map (fun (c : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X])) s))
    (Multiset.prod
      (Multiset.map
        ((fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) ∘ fun (c : E) ↦ c / b) s))
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    Multiset.prod
      (Multiset.map
        ((fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) ∘ fun (c : E) ↦ c / b) s)

Tactic:
rw [key1, hs, multiset_prod_comp, Multiset.map_map, key2, Multiset.prod_map_mul,
    Function.const_def (α := E) (y := C b), Multiset.map_const, Multiset.prod_replicate,
    hs', ← C_pow, hb, ← mul_assoc, C_mul_C, one_mul]

Premises used: Multiset.prod_replicate, mul_assoc, Multiset.map_const, Polynomial.multiset_prod_comp, Multiset.prod_map_mul, Function.const_def, Multiset.map_map, Polynomial.C_pow, one_mul
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_3
inst : Field F
E : Type u_4
inst_1 : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).Splits
ha' : Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)
hn : ¬n = 0
hn' : 0 < n
hn'' : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
b : E
hb : b ^ n = (i : (a : F) → E) a
hb' : b ≠ 0
s : Multiset E := (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).roots
hs :
  map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    Multiset.prod (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
key1 :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
key2 :
  Eq.{u_4 + 1} (α := E → E[X])
    ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
    fun (c : E) ↦
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
⊢ Eq (α := E[X])
    (Multiset.prod
      (Multiset.map (fun (c : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X])) s))
    (Multiset.prod
      (Multiset.map
        ((fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) ∘ fun (c : E) ↦ c / b) s))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
pos :
  ∀ (hx : x = 0),
    IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal
neg :
  ∀ (hx : ¬x = 0),
    IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : x = 0
pos : IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n).Gal
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal

Tactic:
rw [hx, C_0, sub_zero]

Premises used: sub_zero, Polynomial.C_0
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n).Gal

Tactic:
gal_X_pow_isSolvable n

Premises used: gal_X_pow_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : x = 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n).Gal

Tactic:
exact gal_X_pow_isSolvable n

Premises used: gal_X_pow_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
neg :
  Splits (R := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).SplittingField)
    (map
      (algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).SplittingField)
      (HPow.hPow (α := F[X]) X n - 1))
neg₁ : IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
neg₂ :
  IsSolvable.{u_1}
    (Gal (F := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X]))))
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal

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

Premises used: Polynomial.C, HSub.hSub, HPow.hPow, OfNat.ofNat, Polynomial.X, DFunLike.coe, gal_isSolvable_tower
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (R := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).SplittingField)
    (map
      (algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).SplittingField)
      (HPow.hPow (α := F[X]) X n - 1))

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

Premises used: splits_X_pow_sub_one_of_X_pow_sub_C, Polynomial.SplittingField.splits
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Splits (R := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).SplittingField)
    (map
      (algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).SplittingField)
      (HPow.hPow (α := F[X]) X n - 1))

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

Premises used: splits_X_pow_sub_one_of_X_pow_sub_C, Polynomial.SplittingField.splits
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal

Tactic:
gal_X_pow_sub_one_isSolvable n

Premises used: gal_X_pow_sub_one_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal

Tactic:
exact gal_X_pow_sub_one_isSolvable n

Premises used: gal_X_pow_sub_one_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
neg :
  IsSolvable.{u_1}
    (HSub.hSub (β := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
        (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n)
        ((C : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField[X])
            (((algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
                  F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField) :
                (a : F) → (X ^ n - 1).SplittingField)
              x) :
          (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])).Gal
⊢ IsSolvable.{u_1}
    (Gal (F := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X]))))

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

Premises used: Polynomial.map_pow, Polynomial.map_X, Polynomial.map_sub, Polynomial.map_C
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
neg :
  (map (RingHom.id (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1)).Splits
⊢ IsSolvable.{u_1}
    (HSub.hSub (β := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
        (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n)
        ((C : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField[X])
            (((algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
                  F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField) :
                (a : F) → (X ^ n - 1).SplittingField)
              x) :
          (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])).Gal

Tactic:
apply gal_X_pow_sub_C_isSolvable_aux

Premises used: gal_X_pow_sub_C_isSolvable_aux