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

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]

Premises used: Polynomial.map_one, Polynomial.pow_comp, mul_sub, Polynomial.X_comp, mul_assoc, Polynomial.map_pow, Polynomial.map_X, Polynomial.C_comp, Polynomial.map_sub, Polynomial.map_C, mul_pow, Polynomial.C_pow, one_mul, Polynomial.sub_comp