awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
σ τ : (HPow.hPow (α := F[X]) X n - 1).Gal
a : (HPow.hPow (α := F[X]) X n - 1).SplittingField
ha : a ^ n = 1
key :
  ∀ (σ : (HPow.hPow (α := F[X]) X n - 1).Gal),
    ∃ (m : ℕ), (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ m
c : ℕ
hc : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ c
d : ℕ
hd : (τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ d
neg :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ * σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₁ :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₂ :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ c) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₃ :
  (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
      ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) =
    HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
        (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      c
neg₄ : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ d) = (a ^ d) ^ c
neg₅ :
  HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
        (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      d =
    (a ^ d) ^ c
⊢ Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ * τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ * σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
have neg₆ : (a ^ c) ^ d = (a ^ d) ^ c
Tactic: rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
σ τ : (HPow.hPow (α := F[X]) X n - 1).Gal
a : (HPow.hPow (α := F[X]) X n - 1).SplittingField
ha : a ^ n = 1
key :
  ∀ (σ : (HPow.hPow (α := F[X]) X n - 1).Gal),
    ∃ (m : ℕ), (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ m
c : ℕ
hc : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ c
d : ℕ
hd : (τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ d
neg :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ * σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₁ :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₂ :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ c) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₃ :
  (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
      ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) =
    HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
        (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      c
neg₄ : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ d) = (a ^ d) ^ c
neg₅ :
  HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
        (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      d =
    (a ^ d) ^ c
neg₆ : (a ^ c) ^ d = (a ^ d) ^ c
⊢ Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ * τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ * σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
have neg₇ : a ^ (c * d) = (a ^ d) ^ c
Tactic: rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
σ τ : (HPow.hPow (α := F[X]) X n - 1).Gal
a : (HPow.hPow (α := F[X]) X n - 1).SplittingField
ha : a ^ n = 1
key :
  ∀ (σ : (HPow.hPow (α := F[X]) X n - 1).Gal),
    ∃ (m : ℕ), (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ m
c : ℕ
hc : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ c
d : ℕ
hd : (τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ d
neg :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ * σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₁ :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₂ :
  Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
        ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ c) :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
neg₃ :
  (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField)
      ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a) =
    HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
        (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      c
neg₄ : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ d) = (a ^ d) ^ c
neg₅ :
  HPow.hPow (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
        (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      d =
    (a ^ d) ^ c
neg₆ : (a ^ c) ^ d = (a ^ d) ^ c
neg₇ : a ^ (c * d) = (a ^ d) ^ c
⊢ Eq (α := (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((σ * τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((τ * σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a :
      (HPow.hPow (α := F[X]) X n - 1).SplittingField)
have neg₈ : (a ^ d) ^ c = (a ^ d) ^ c
Tactic: rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have pos : ∀ (ha : a = 0), IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
pos :
  ∀ (ha : a = 0),
    IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have neg : ∀ (ha : ¬a = 0),
  IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : a = 0
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have pos : IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n).Gal
Tactic: rw [ha, C_0, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have ha' : Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
  ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
        (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
      a :
    (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
  (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
Tactic: have ha' : algebraMap F (X ^ n - C a).SplittingField a ≠ 0 :=
    mt ((injective_iff_map_eq_zero _).mp (RingHom.injective _) a) ha
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have pos : ∀ (hn : n = 0), IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
pos :
  ∀ (hn : n = 0),
    IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have neg : ∀ (hn : ¬n = 0),
  IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
hn : n = 0
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have pos : IsSolvable.{u_1} (Gal (F := F) ((C : (a : F) → F[X]) (1 - a)))
Tactic: rw [hn, pow_zero, ← C_1, ← C_sub]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
hn : ¬n = 0
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have hn' : 0 < n
Tactic: have hn' : 0 < n := pos_iff_ne_zero.mpr hn
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have hn'' : HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]) ≠ 0
Tactic: have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
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]) ≠ 0
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
have hn''' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
Tactic: have hn''' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
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]) ≠ 0
hn''' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
c : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField
hc : c ^ n = 1
⊢ Eq (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((aeval c : (a_1 : F[X]) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)) :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
have rwa : Eq (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
  ((aeval c : (a_1 : F[X]) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField) (HPow.hPow (α := F[X]) X n - 1) :
    (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
  (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
Tactic: rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
ha' :
  Ne (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((algebraMap F (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
          (a_1 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        a :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
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]) ≠ 0
hn''' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
c : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField
hc : c ^ n = 1
rwa :
  Eq (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((aeval c : (a_1 : F[X]) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField) (HPow.hPow (α := F[X]) X n - 1) :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
⊢ Eq (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((aeval c : (a_1 : F[X]) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
        (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)) :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (0 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
have rwa₁ : HSub.hSub (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (β := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((aeval c : (a_1 : F[X]) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField) (HPow.hPow (α := F[X]) X n) :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    ((aeval c : (a_1 : F[X]) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField) 1 :
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField) =
  0
Tactic: rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one]