awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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))
c : E
h₁ :
  comp X (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) -
      comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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]))
⊢ (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X])).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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]))
have h₂ : HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X -
    comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
  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: rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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))
c : E
h₁ :
  comp X (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) -
      comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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₂ :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X -
      comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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]))
⊢ (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X])).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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]))
have h₃ : HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
    ((C : (a : E) → E[X]) c : E[X]) =
  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: rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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))
c : E
h₁ :
  comp X (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) -
      comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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₂ :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X -
      comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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₃ :
  HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) c : E[X]) =
    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]))
⊢ (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X])).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    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]))
have h₄ : HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
    ((C : (a : E) → E[X]) c : E[X]) =
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X -
    HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) ((C : (a : E) → E[X]) (c / b) : E[X])
Tactic: rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
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))
⊢ 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)
have 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]))
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']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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]))
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal
have 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
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal
have 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
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
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
have pos : IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n).Gal
Tactic: rw [hx, C_0, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
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
have 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))
Tactic: apply gal_isSolvable_tower (X ^ n - 1) (X ^ n - C x)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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))
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal
have neg₁ : IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
Tactic: apply gal_isSolvable_tower (X ^ n - 1) (X ^ n - C x)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Gal
have 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]))))
Tactic: apply gal_isSolvable_tower (X ^ n - 1) (X ^ n - C x)
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ 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]))))
have 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
Tactic: rw [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ 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
have 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
Tactic: apply gal_X_pow_sub_C_isSolvable_aux
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ (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
have neg : (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
Tactic: rw [map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
have key : Splits (R := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
  (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n - 1))
Tactic: have key := SplittingField.splits (X ^ n - 1 : F[X])
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
key :
  Splits (R := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n - 1))
⊢ (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
have neg : ∀
  (key :
    (HSub.hSub (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
        (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n))
        (map
          (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
            F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
          1)).Splits),
  (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
Tactic: rwa [Polynomial.map_sub, Polynomial.map_pow, map_X,
      Polynomial.map_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
key :
  Splits (R := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n - 1))
neg :
  ∀
    (key :
      (HSub.hSub (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
          (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n))
          (map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            1)).Splits),
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
⊢ (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
have neg₁ : ∀
  (key :
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
          (map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            X)
          n -
        map
          (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
            F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
          1).Splits),
  (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
Tactic: rwa [Polynomial.map_sub, Polynomial.map_pow, map_X,
      Polynomial.map_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
x : F
hx : ¬x = 0
key :
  Splits (R := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n - 1))
neg :
  ∀
    (key :
      (HSub.hSub (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
          (map (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField) (HPow.hPow (α := F[X]) X n))
          (map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            1)).Splits),
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
neg₁ :
  ∀
    (key :
      (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X])
            (map
              (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
                F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
              X)
            n -
          map
            (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
              F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
            1).Splits),
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
⊢ (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
have neg₂ : ∀
  (key :
    (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n -
        map
          (algebraMap F (HPow.hPow (α := F[X]) X n - 1).SplittingField :
            F →+* (HPow.hPow (α := F[X]) X n - 1).SplittingField)
          1).Splits),
  (HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField[X]) X n - 1).Splits
Tactic: rwa [Polynomial.map_sub, Polynomial.map_pow, map_X,
      Polynomial.map_one] at key
Cleared hypotheses: key