-- 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
key :
  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
c : F
hc :
  (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 =
    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
h₁ :
  (σ : (a_1 : (X ^ n - (C : (a : F) → F[X]) a).SplittingField) → (X ^ n - (C : (a : F) → F[X]) a).SplittingField) b =
    b *
      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
h₂ h₃ :
  Eq (α := (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)
    ((σ : (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)
⊢ (σ : (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:
rw [hc, mul_div_cancel₀ (σ b) hb']

Premises used: mul_div_cancel₀, DFunLike.coe