awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AbelRuffini
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
neg₈ neg₉ : (a ^ d) ^ c = (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)

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

Premises used: map_pow, pow_mul, AlgEquiv.mul_apply, pow_mul'
-- Module: Mathlib.FieldTheory.AbelRuffini
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
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
⊢ 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
-- Module: Mathlib.FieldTheory.AbelRuffini
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
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]) a : F[X])).Gal

Tactic:
rw [ha, C_0, sub_zero]

Premises used: sub_zero, Polynomial.C_0
-- Module: Mathlib.FieldTheory.AbelRuffini
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} (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 : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : a = 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 : ℕ
a : F
h : (map (RingHom.id F) (HPow.hPow (α := F[X]) X n - 1)).Splits
ha : ¬a = 0
⊢ 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
-- Module: Mathlib.FieldTheory.AbelRuffini
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
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
⊢ 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
-- Module: Mathlib.FieldTheory.AbelRuffini
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
pos : IsSolvable.{u_1} (Gal (F := F) ((C : (a : F) → F[X]) (1 - a)))
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal

Tactic:
rw [hn, pow_zero, ← C_1, ← C_sub]

Premises used: Polynomial.C_1, Polynomial.C_sub, pow_zero
-- Module: Mathlib.FieldTheory.AbelRuffini
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} (Gal (F := F) ((C : (a : F) → F[X]) (1 - a)))

Tactic:
gal_C_isSolvable (1 - a)

Premises used: HSub.hSub, gal_C_isSolvable, OfNat.ofNat
-- Module: Mathlib.FieldTheory.AbelRuffini
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} (Gal (F := F) ((C : (a : F) → F[X]) (1 - a)))

Tactic:
exact gal_C_isSolvable (1 - a)

Premises used: HSub.hSub, gal_C_isSolvable, OfNat.ofNat
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ 0 < n

Tactic:
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ 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
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ 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
-- Module: Mathlib.FieldTheory.AbelRuffini
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},
    c ^ n = 1 →
      ∃ (d : F),
        (algebraMap F
                (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
              (a_2 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
            d =
          c

Tactic:
have mem_range : ∀ {c : (X ^ n - C a).SplittingField},
      (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) := fun {c} hc =>
    RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c
      (Splits.degree_eq_one_of_irreducible (h.of_dvd (map_ne_zero hn''')
        (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))
          (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))))
-- Module: Mathlib.FieldTheory.AbelRuffini
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
mem_range :
  ∀ {c : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField},
    c ^ n = 1 →
      ∃ (d : F),
        (algebraMap F
                (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
              (a_2 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
            d =
          c
neg :
  ∀ (a_1 b : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal), a_1 * b = b * a_1
⊢ IsSolvable.{u_1} (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal

Tactic:
apply isSolvable_of_comm

Premises used: isSolvable_of_comm
-- Module: Mathlib.FieldTheory.AbelRuffini
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
mem_range :
  ∀ {c : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField},
    c ^ n = 1 →
      ∃ (d : F),
        (algebraMap F
                (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
              (a_2 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
            d =
          c
σ τ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
neg :
  ∀ (b : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    (hb :
      Membership.mem (γ :=
        Set (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])).rootSet
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
        b),
    Eq (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
      ((σ * τ :
            (a_1 : (X ^ n - (C : (a : F) → F[X]) a).SplittingField) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
          b :
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
      ((τ * σ :
            (a_1 : (X ^ n - (C : (a : F) → F[X]) a).SplittingField) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
          b :
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
⊢ σ * τ = τ * σ

Tactic:
ext b hb
-- Module: Mathlib.FieldTheory.AbelRuffini
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
mem_range :
  ∀ {c : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField},
    c ^ n = 1 →
      ∃ (d : F),
        (algebraMap F
                (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
              (a_2 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
            d =
          c
σ τ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
b : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField
hb :
  Membership.mem (γ :=
    Set (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])).rootSet
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
    b
⊢ b ^ n =
    (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

Tactic:
rw [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb

Premises used: map_sub, sub_eq_zero, Polynomial.aeval_X_pow, Polynomial.aeval_C, Polynomial.mem_rootSet_of_ne
-- Module: Mathlib.FieldTheory.AbelRuffini
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
mem_range :
  ∀ {c : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField},
    c ^ n = 1 →
      ∃ (d : F),
        (algebraMap F
                (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField :
              (a_2 : F) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
            d =
          c
σ τ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
b : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField
hb :
  b ^ n =
    (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
hb' : b = 0
⊢ Eq (α := (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)
    ((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)

Tactic:
rw [hb', zero_pow hn] at hb

Premises used: zero_pow