awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p)
hp : IsSolvable.{u_1} p.Gal
hq : IsSolvable.{u_1} (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) q))
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := AlgEquiv.autCongr (IsSplittingField.algEquiv L (map (algebraMap F K) q))
ϕ_inj :
  Function.Injective (α := Gal(L/K)) (β := (map (algebraMap F K) q).Gal)
    (⇑ϕ.toMonoidHom : (a : Gal(L/K)) → (map (algebraMap F K) q).Gal)
⊢ IsSolvable.{u_1} q.Gal
have this₁ : IsSolvable.{u_1} Gal(K/F)
Tactic: haveI : IsSolvable Gal(K/F) := hp
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p)
hp : IsSolvable.{u_1} p.Gal
hq : IsSolvable.{u_1} (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) q))
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this_1 : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := AlgEquiv.autCongr (IsSplittingField.algEquiv L (map (algebraMap F K) q))
ϕ_inj :
  Function.Injective (α := Gal(L/K)) (β := (map (algebraMap F K) q).Gal)
    (⇑ϕ.toMonoidHom : (a : Gal(L/K)) → (map (algebraMap F K) q).Gal)
this : IsSolvable.{u_1} Gal(K/F)
⊢ IsSolvable.{u_1} q.Gal
have this₁ : IsSolvable.{u_1} Gal(L/K)
Tactic: haveI : IsSolvable Gal(L/K) := solvable_of_solvable_injective ϕ_inj
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
n : ℕ
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
have pos : ∀ (hn : n = 0), IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).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 : ℕ
pos : ∀ (hn : n = 0), IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
have neg : ∀ (hn : ¬n = 0), IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).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 : ℕ
hn : n = 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
have pos : IsSolvable.{u_1} (Gal (F := F) 0)
Tactic: rw [hn, pow_zero, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : ¬n = 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).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 : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).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 : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
have neg : ∀ (a b : (HPow.hPow (α := F[X]) X n - 1).Gal), a * b = b * a
Tactic: apply isSolvable_of_comm
-- 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
⊢ σ * τ = τ * σ
have neg : ∀ (a : (HPow.hPow (α := F[X]) X n - 1).SplittingField)
  (ha :
    Membership.mem (γ := Set (HPow.hPow (α := F[X]) X n - 1).SplittingField)
      ((HPow.hPow (α := F[X]) X n - 1).rootSet (HPow.hPow (α := F[X]) X n - 1).SplittingField) a),
  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: ext a ha
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
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 :
  Membership.mem (γ := Set (HPow.hPow (α := F[X]) X n - 1).SplittingField)
    ((HPow.hPow (α := F[X]) X n - 1).rootSet (HPow.hPow (α := F[X]) X n - 1).SplittingField) a
⊢ 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 ha₁ : a ^ n = 1
Tactic: simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha
Cleared hypotheses: ha
-- 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
σ_1 τ : (HPow.hPow (α := F[X]) X n - 1).Gal
a : (HPow.hPow (α := F[X]) X n - 1).SplittingField
ha : a ^ n = 1
σ : (HPow.hPow (α := F[X]) X n - 1).Gal
⊢ ∃ (m : ℕ), (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ m
have lift : ∀ (n : ℕ+) (hn : ¬(↑n : ℕ) = 0) (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) (σ : (HPow.hPow (α := F[X]) X (↑n : ℕ) - 1).Gal),
  ∃ (m : ℕ), (σ : (a : (X ^ (↑n : ℕ) - 1).SplittingField) → (X ^ (↑n : ℕ) - 1).SplittingField) a = a ^ m
Tactic: lift n to ℕ+ using hn'
Cleared hypotheses: n, hn, hn', hn'', σ_1, τ, a, ha, σ
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
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
⊢ 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 key : ∀ (σ : (HPow.hPow (α := F[X]) X n - 1).Gal),
  ∃ (m : ℕ), (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ m
Tactic: have key : ∀ σ : (X ^ n - 1 : F[X]).Gal, ∃ m : ℕ, σ a = a ^ m := by
    intro σ
    lift n to ℕ+ using hn'
    exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)
-- 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
⊢ 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 : ∀ (c : ℕ) (hc : (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ 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: obtain ⟨c, hc⟩ := key σ
-- 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
⊢ 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 : ∀ (d : ℕ) (hd : (τ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ d),
  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: obtain ⟨d, hd⟩ := key τ
-- 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
⊢ 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 : 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)
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)
⊢ 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₁ : 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)
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)
⊢ 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₂ : 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)
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)
⊢ 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 : (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
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
⊢ 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 : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) (a ^ 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
⊢ 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₅ : 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
Tactic: rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']