awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
rw :
  Eq (α := E[X])
    ((C : (a : E) → E[X]) (HMul.hMul (α := E) (β := E) ((i : (a : F) → E) a⁻¹ : E) ((i : (a : F) → E) a : E)) : E[X])
    (1 : E[X])
rw₁ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) (a⁻¹ * a)) : E[X]) (1 : E[X])
rw₂ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) 1)) 1
⊢ HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
have rw₃ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) 1) 1
Tactic: rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
rw :
  Eq (α := E[X])
    ((C : (a : E) → E[X]) (HMul.hMul (α := E) (β := E) ((i : (a : F) → E) a⁻¹ : E) ((i : (a : F) → E) a : E)) : E[X])
    (1 : E[X])
rw₁ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) (a⁻¹ * a)) : E[X]) (1 : E[X])
rw₂ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) 1)) 1
rw₃ : Eq.{u_4 + 1} (α := E[X]) ((C : (a : E) → E[X]) 1) 1
⊢ HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
have rw₄ : Eq.{u_4 + 1} (α := E[X]) 1 1
Tactic: rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
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)
hs' : s.card = n
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    Multiset.prod
      (Multiset.map
        ((fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) ∘ fun (c : E) ↦ c / b) s)
have C_mul_C : HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
  1
Tactic: have C_mul_C : C (i a⁻¹) * C (i a) = 1 := by
    rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
have rw : map i (HPow.hPow (α := F[X]) X n) - map i 1 =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
Tactic: rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
rw :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
have rw₁ : map i (HPow.hPow (α := F[X]) X n) - map i 1 =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((map i (HPow.hPow (α := F[X]) X n) - map i ((C : (a : F) → F[X]) a)).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
Tactic: rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
rw :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
rw₁ :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HPow.hPow (α := F[X]) X n) - map i ((C : (a : F) → F[X]) a)).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
have rw₂ : map i X ^ n - map i 1 =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((map i X ^ n - map i ((C : (a : F) → F[X]) a)).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
Tactic: rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
rw :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
rw₁ :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HPow.hPow (α := F[X]) X n) - map i ((C : (a : F) → F[X]) a)).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
rw₂ :
  map i X ^ n - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i X ^ n - map i ((C : (a : F) → F[X]) a)).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
have rw₃ : HPow.hPow (α := E[X]) X n - map i 1 =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((HPow.hPow (α := E[X]) X n - map i ((C : (a : F) → F[X]) a)).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
Tactic: rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
rw :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
rw₁ :
  map i (HPow.hPow (α := F[X]) X n) - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HPow.hPow (α := F[X]) X n) - map i ((C : (a : F) → F[X]) a)).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
rw₂ :
  map i X ^ n - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i X ^ n - map i ((C : (a : F) → F[X]) a)).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
rw₃ :
  HPow.hPow (α := E[X]) X n - map i 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((HPow.hPow (α := E[X]) X n - map i ((C : (a : F) → F[X]) a)).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
have rw₄ : HPow.hPow (α := E[X]) X n - map i 1 =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X n) ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X])).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
Tactic: rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
⊢ map i (HPow.hPow (α := F[X]) X n - 1) =
    Multiset.prod
      (Multiset.map
        ((fun (x : E) ↦ HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X])) ∘ fun (c : E) ↦ c / b) s)
have key1 : map i (HPow.hPow (α := F[X]) X n - 1) =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
Tactic: have key1 : (X ^ n - 1 : F[X]).map i = C (i a⁻¹) * ((X ^ n - C a).map i).comp (C b * X) := by
    rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
key1 :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
⊢ Eq.{u_4 + 1} (α := E → E[X])
    ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
    fun (c : E) ↦
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
have h₁ : ∀ (c : E),
  ((fun (q : E[X]) ↦ q.comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)) ∘ fun (c : E) ↦
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X]))
      c =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
Tactic: ext1 c
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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)
hs' : s.card = n
C_mul_C :
  HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((C : (a : E) → E[X]) ((i : (a : F) → E) a) : E[X]) =
    1
key1 :
  map i (HPow.hPow (α := F[X]) X n - 1) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((map i (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X]))).comp
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X))
c : E
⊢ (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) c : E[X])).comp
      (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
have h₁ : comp X (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) -
    comp ((C : (a : E) → E[X]) c) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) b : E[X])
    (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (c / b) : E[X]))
Tactic: rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']