awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hb₁ :
  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)
⊢ b = 0

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

Premises used: zero_pow
-- 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 :
  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)
hb' : b = 0
⊢ False

Tactic:
ha' hb.symm

Premises used: Eq.symm
-- 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 :
  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)
hb' : b = 0
⊢ False

Tactic:
exact ha' hb.symm

Premises used: Eq.symm
-- 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
⊢ b ≠ 0

Tactic:
have hb' : b ≠ 0 := by
    intro hb'
    rw [hb', zero_pow hn] at hb
    exact ha' hb.symm
-- 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
σ_1 τ : (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
σ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal
⊢ HDiv.hDiv (α := (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)
        b ^
      n =
    1

Tactic:
have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← map_pow, hb, σ.commutes, div_self 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)
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
⊢ ∀ (σ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Gal),
    ∃ (c : F),
      (σ : (a_1 : (X ^ n - (C : (a : F) → F[X]) a).SplittingField) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField)
          b =
        HMul.hMul (β :=
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField) b
          ((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)
              c :
            (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)

Tactic:
have key : ∀ σ : (X ^ n - C a).Gal, ∃ c, σ b = b * algebraMap F _ c := by
    intro σ
    have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← map_pow, hb, σ.commutes, div_self ha']
    obtain ⟨c, hc⟩ := mem_range key
    use c
    rw [hc, mul_div_cancel₀ (σ b) hb']
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ Ne.{u_4 + 1} (α := E) ((i : (a : F) → E) a : E) (0 : E)

Tactic:
have ha' : i a ≠ 0 := mt ((injective_iff_map_eq_zero i).mp i.injective a) ha
-- Module: Mathlib.FieldTheory.AbelRuffini
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)
pos : ∀ (hn : n = 0), (map i (HPow.hPow (α := F[X]) X n - 1)).Splits
neg : ∀ (hn : ¬n = 0), (map i (HPow.hPow (α := F[X]) X n - 1)).Splits
⊢ (map i (HPow.hPow (α := F[X]) X n - 1)).Splits

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ (map i (HPow.hPow (α := F[X]) X n - 1)).Splits

Tactic:
simp [hn]
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ 0 < n

Tactic:
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0

Tactic:
have hn'' : (X ^ n - C a).degree ≠ 0 :=
    ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt WithBot.coe_eq_coe.mp hn)
-- Module: Mathlib.FieldTheory.AbelRuffini
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
rwa rwa₁ rwa₂ rwa₃ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).degree ≠ 0
⊢ (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).degree ≠ 0

Tactic:
rwa [degree_map]

Premises used: Polynomial.degree_map
-- Module: Mathlib.FieldTheory.AbelRuffini
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
neg :
  ∀ (b : E)
    (hb : eval b (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))) = 0),
    (map i (HPow.hPow (α := F[X]) X n - 1)).Splits
⊢ (map i (HPow.hPow (α := F[X]) X n - 1)).Splits

Tactic:
obtain ⟨b, hb⟩ := Splits.exists_eval_eq_zero h (by rwa [degree_map])

Premises used: Polynomial.Splits.exists_eval_eq_zero
-- Module: Mathlib.FieldTheory.AbelRuffini
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 : eval b (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))) = 0
⊢ b ^ n = (i : (a : F) → E) a

Tactic:
rw [eval_map, eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at hb

Premises used: Polynomial.eval_map, Polynomial.eval₂_X_pow, sub_eq_zero, Polynomial.eval₂_sub, Polynomial.eval₂_C
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ Eq.{u_4 + 1} (α := E) (0 : E) ((i : (a : F) → E) a : E)

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

Premises used: zero_pow
-- Module: Mathlib.FieldTheory.AbelRuffini
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
hb₁ : Eq.{u_4 + 1} (α := E) (0 : E) ((i : (a : F) → E) a : E)
⊢ b = 0

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

Premises used: zero_pow
-- Module: Mathlib.FieldTheory.AbelRuffini
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 : Eq.{u_4 + 1} (α := E) (0 : E) ((i : (a : F) → E) a : E)
hb' : b = 0
⊢ False

Tactic:
ha' hb.symm

Premises used: Eq.symm
-- Module: Mathlib.FieldTheory.AbelRuffini
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 : Eq.{u_4 + 1} (α := E) (0 : E) ((i : (a : F) → E) a : E)
hb' : b = 0
⊢ False

Tactic:
exact ha' hb.symm

Premises used: Eq.symm
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ b ≠ 0

Tactic:
have hb' : b ≠ 0 := by
    intro hb'
    rw [hb', zero_pow hn] at hb
    exact ha' hb.symm
-- Module: Mathlib.FieldTheory.AbelRuffini
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
⊢ map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])) =
    HMul.hMul (α := E[X]) (β := E[X])
      ((C : (a : E) → E[X])
          (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).leadingCoeff :
        E[X])
      (Multiset.prod
          (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s) :
        E[X])

Tactic:
have hs : _ = _ * (s.map _).prod := h.eq_prod_roots
-- Module: Mathlib.FieldTheory.AbelRuffini
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])) =
    HMul.hMul (α := E[X]) (β := E[X])
      ((C : (a : E) → E[X])
          (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).leadingCoeff :
        E[X])
      (Multiset.prod
          (Multiset.map (fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) s) :
        E[X])
⊢ 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)

Tactic:
rw [leadingCoeff_map, leadingCoeff_X_pow_sub_C hn', RingHom.map_one, C_1, one_mul] at hs

Premises used: Polynomial.C_1, RingHom.map_one, Polynomial.leadingCoeff_X_pow_sub_C, Polynomial.leadingCoeff_map, one_mul
-- Module: Mathlib.FieldTheory.AbelRuffini
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)
rw : (map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).natDegree = n
rw₁ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).natDegree = n
rw₂ rw₃ : n = n
⊢ s.card = n

Tactic:
rw [← h.natDegree_eq_card_roots, natDegree_map, natDegree_X_pow_sub_C]

Premises used: Polynomial.natDegree_X_pow_sub_C, Polynomial.natDegree_map, Polynomial.Splits.natDegree_eq_card_roots