-- 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)
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
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]))
h₂ :
  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]))
h₃ :
  HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) c : E[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]))
h₄ :
  HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) c : E[X]) =
    HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X -
      HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) ((C : (a : E) → E[X]) (c / b) : E[X])
h₅ :
  HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) c : E[X]) =
    HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) (b * (c / b)) : E[X])
h₆ h₇ :
  HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) c : E[X]) =
    HSub.hSub (β := E[X]) (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) b : E[X]) X)
      ((C : (a : E) → E[X]) c : E[X])
⊢ (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]))

Tactic:
rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']

Premises used: mul_sub, Polynomial.X_comp, mul_div_cancel₀, Polynomial.C_comp, Polynomial.C_mul, Polynomial.sub_comp