awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
⊢ IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)

Tactic:
fun hU _ ↦ h₄ (isOpen_iUnion fun a ↦ hU.preimage (h.1 a)) ?_ fun b _ ↦ ?_

Premises used: ContinuousConstSMul.continuous_const_smul, isOpen_iUnion, IsOpen.preimage
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
refine_1 :
  ∀ {U : Set α} (hU : IsOpen U), U.Nonempty → Set.Nonempty.{u_2} (α := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
refine_2 :
  ∀ {U : Set α} (hU : IsOpen U),
    U.Nonempty →
      ∀ (b : M) (x : α),
        Membership.mem (γ := Set α) (preimage (β := α) (fun (x : α) ↦ b • x) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U))
            x →
          Membership.mem (γ := Set α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U) x
⊢ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)

Tactic:
refine fun hU _ ↦ h₄ (isOpen_iUnion fun a ↦ hU.preimage (h.1 a)) ?_ fun b _ ↦ ?_

Premises used: isOpen_iUnion
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
hU : IsOpen U
h_1 : U.Nonempty
⊢ Set.Nonempty (α := α) ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x) ⁻¹' U)

Tactic:
simpa only [one_smul]

Premises used: one_smul
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
hU : IsOpen U
h_1 : U.Nonempty
⊢ Set.Nonempty.{u_2} (α := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)

Tactic:
exact nonempty_iUnion.mpr ⟨1, by simpa only [one_smul]⟩

Premises used: Iff.mpr, Set.nonempty_iUnion, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
hU : IsOpen U
h_1 : U.Nonempty
b : M
x : α
refine_2 : ∀ (x_1 : M) (h : (x_1 * b) • x ∈ U), ∃ (i : M), i • x ∈ U
⊢ Membership.mem (γ := Set α) (preimage (β := α) (fun (x : α) ↦ b • x) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)) x →
    Membership.mem (γ := Set α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U) x

Tactic:
simp only [preimage_iUnion, mem_iUnion, mem_preimage, smul_smul, forall_exists_index]

Premises used: Set.mem_iUnion, forall_exists_index, smul_smul, Set.preimage_iUnion, Set.mem_preimage
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
hU : IsOpen U
h_1 : U.Nonempty
b : M
x : α
⊢ ∀ (x_1 : M) (h : (x_1 * b) • x ∈ U), ∃ (i : M), i • x ∈ U

Tactic:
fun c hc ↦ ⟨c * b, hc⟩

Premises used: HMul.hMul, Exists.intro
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
hU : IsOpen U
h_1 : U.Nonempty
b : M
x : α
⊢ ∀ (x_1 : M) (h : (x_1 * b) • x ∈ U), ∃ (i : M), i • x ∈ U

Tactic:
exact fun c hc ↦ ⟨c * b, hc⟩
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : IsMinimal M α
⊢ IsTopologicallyTransitive M α

Tactic:
(isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr fun h hn ↦ ?_

Premises used: Iff.mpr, MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : IsMinimal M α
refine : ∀ {U : Set α} (h : IsOpen U) (hn : U.Nonempty), Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
⊢ IsTopologicallyTransitive M α

Tactic:
refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr fun h hn ↦ ?_

Premises used: Iff.mpr, MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : IsMinimal M α
U : Set α
h : IsOpen U
hn : U.Nonempty
⊢ Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)

Tactic:
simp only [h.iUnion_preimage_smul M hn, dense_univ]

Premises used: dense_univ, IsOpen.iUnion_preimage_smul
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
⊢ IsSolvable.{u_1} (Gal (F := F) 0)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
⊢ IsSolvable.{u_1} (Gal (F := F) 1)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
x : F
⊢ IsSolvable.{u_1} (Gal (F := F) ((C : (a : F) → F[X]) x))

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
⊢ IsSolvable.{u_1} (Gal (F := F) X)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
x : F
⊢ IsSolvable.{u_1} (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])).Gal

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n).Gal

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
p q : F[X]
h : IsSolvable.{u_1} p.Gal
h_1 : IsSolvable.{u_1} q.Gal
⊢ IsSolvable.{u_1} (p * q).Gal

Tactic:
solvable_of_solvable_injective (Gal.restrictProd_injective p q)

Premises used: solvable_of_solvable_injective, Polynomial.Gal.restrictProd_injective
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
h₁ : IsSolvable.{u_1} (Gal (F := F) (Multiset.prod 0))
h₂ :
  ∀ {a : F[X]} {s_1 : Multiset F[X]},
    a ∈ s → s_1 ⊆ s → IsSolvable.{u_1} s_1.prod.Gal → IsSolvable.{u_1} (insert a s_1).prod.Gal
⊢ IsSolvable.{u_1} s.prod.Gal

Tactic:
apply Multiset.induction_on' s

Premises used: Multiset.induction_on'
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
⊢ IsSolvable.{u_1} (Gal (F := F) (Multiset.prod 0))

Tactic:
gal_one_isSolvable

Premises used: Multiset.foldr, Multiset.prod, gal_one_isSolvable, List.foldr
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
⊢ IsSolvable.{u_1} (Gal (F := F) (Multiset.prod 0))

Tactic:
exact gal_one_isSolvable

Premises used: gal_one_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
h₂ : t ⊆ s → IsSolvable.{u_1} t.prod.Gal → IsSolvable.{u_1} (insert p t).prod.Gal
⊢ t ⊆ s → IsSolvable.{u_1} t.prod.Gal → IsSolvable.{u_1} (insert p t).prod.Gal

Tactic:
_
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
h : t ⊆ s
ht : IsSolvable.{u_1} t.prod.Gal
h₂ : IsSolvable.{u_1} (p * t.prod).Gal
⊢ IsSolvable.{u_1} (insert p t).prod.Gal

Tactic:
rw [Multiset.insert_eq_cons, Multiset.prod_cons]

Premises used: Multiset.prod_cons, Multiset.insert_eq_cons
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
h : t ⊆ s
ht : IsSolvable.{u_1} t.prod.Gal
⊢ IsSolvable.{u_1} (p * t.prod).Gal

Tactic:
gal_mul_isSolvable (hs p hps) ht

Premises used: gal_mul_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
h : t ⊆ s
ht : IsSolvable.{u_1} t.prod.Gal
⊢ IsSolvable.{u_1} (p * t.prod).Gal

Tactic:
exact gal_mul_isSolvable (hs p hps) ht

Premises used: gal_mul_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
p q : F[X]
h : Fact (Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p))
hq : IsSolvable.{u_1} q.Gal
⊢ IsSolvable.{u_1} p.Gal

Tactic:
haveI : IsSolvable (q.SplittingField ≃ₐ[F] q.SplittingField) := hq
  solvable_of_surjective (AlgEquiv.restrictNormalHom_surjective q.SplittingField)

Premises used: solvable_of_surjective, AlgEquiv.restrictNormalHom_surjective, Polynomial.SplittingField
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ Fact (map (algebraMap F L) p).Splits

Tactic:
haveI : Fact ((p.map (algebraMap F L)).Splits) := ⟨hpq⟩
-- Module: Mathlib.FieldTheory.AbelRuffini
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))
⊢ Function.Injective (α := Gal(L/K)) (β := (map (algebraMap F K) q).Gal)
    (⇑ϕ.toMonoidHom : (a : Gal(L/K)) → (map (algebraMap F K) q).Gal)

Tactic:
have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective
-- Module: Mathlib.FieldTheory.AbelRuffini
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} Gal(K/F)

Tactic:
haveI : IsSolvable Gal(K/F) := hp
-- Module: Mathlib.FieldTheory.AbelRuffini
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} Gal(L/K)

Tactic:
haveI : IsSolvable Gal(L/K) := solvable_of_solvable_injective ϕ_inj
-- Module: Mathlib.FieldTheory.AbelRuffini
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_2 : IsSolvable.{u_1} Gal(K/F)
this : IsSolvable.{u_1} Gal(L/K)
⊢ IsSolvable.{u_1} q.Gal

Tactic:
isSolvable_of_isScalarTower F p.SplittingField q.SplittingField

Premises used: Polynomial.Gal, Polynomial.SplittingField, isSolvable_of_isScalarTower
-- Module: Mathlib.FieldTheory.AbelRuffini
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_2 : IsSolvable.{u_1} Gal(K/F)
this : IsSolvable.{u_1} Gal(L/K)
⊢ IsSolvable.{u_1} q.Gal

Tactic:
exact isSolvable_of_isScalarTower F p.SplittingField q.SplittingField

Premises used: Polynomial.SplittingField, isSolvable_of_isScalarTower
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
pos : ∀ (hn : n = 0), IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal
neg : ∀ (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

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : n = 0
pos : IsSolvable.{u_1} (Gal (F := F) 0)
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal

Tactic:
rw [hn, pow_zero, sub_self]

Premises used: sub_self, pow_zero
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : n = 0
⊢ IsSolvable.{u_1} (Gal (F := F) 0)

Tactic:
gal_zero_isSolvable

Premises used: gal_zero_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
hn : n = 0
⊢ IsSolvable.{u_1} (Gal (F := F) 0)

Tactic:
exact gal_zero_isSolvable

Premises used: gal_zero_isSolvable
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ
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 : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ 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 : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : HPow.hPow (α := F[X]) X n - 1 ≠ 0
neg : ∀ (a b : (HPow.hPow (α := F[X]) X n - 1).Gal), a * b = b * a
⊢ IsSolvable.{u_1} (HPow.hPow (α := F[X]) X n - 1).Gal

Tactic:
apply isSolvable_of_comm

Premises used: isSolvable_of_comm
-- 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
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
-- 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 :
  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
⊢ a ^ n = 1

Tactic:
simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha

Premises used: map_sub, sub_eq_zero, Polynomial.aeval_X_pow, Polynomial.aeval_one, Polynomial.mem_rootSet_of_ne
-- 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
σ_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
⊢ 0 < n

Tactic:
hn'
-- 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
σ_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
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
⊢ ∃ (m : ℕ), (σ : (a : (X ^ n - 1).SplittingField) → (X ^ n - 1).SplittingField) a = a ^ m

Tactic:
lift n to ℕ+ using hn'
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ+
hn : ¬(↑n : ℕ) = 0
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

Tactic:
map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)

Premises used: AlgEquiv.toAlgHom, map_rootsOfUnity_eq_pow_self, rootsOfUnity.mkOfPowEq
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
inst : Field F
n : ℕ+
hn : ¬(↑n : ℕ) = 0
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

Tactic:
exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)

Premises used: AlgEquiv.toAlgHom, map_rootsOfUnity_eq_pow_self, rootsOfUnity.mkOfPowEq
-- 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
⊢ ∀ (σ : (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)
-- 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
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)
⊢ 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 σ
-- 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
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)
⊢ 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 τ