-- 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))
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))
rw₅ :
  HPow.hPow (α := E[X]) X n - 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))
rw₆ :
  HPow.hPow (α := E[X]) X n - 1 =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
      ((HPow.hPow (α := E[X]) X n).comp (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) -
        comp ((C : (a : E) → E[X]) ((i : (a : F) → E) a))
          (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 - 1 =
  HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) ((i : (a : F) → E) a⁻¹) : E[X])
    (comp X (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X) ^ n -
      comp ((C : (a : E) → E[X]) ((i : (a : F) → E) a))
        (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]