-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
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
rw :
  HPow.hPow (α := (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)
        n /
      b ^ n =
    1
rw₁ :
  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 ^ n) :
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
      (b ^ n) =
    1
rw₂ :
  HDiv.hDiv (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
      (β := (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)
          ((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)
      ((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) =
    1
rw₃ :
  HDiv.hDiv (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField)
      (β := (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)
      ((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) =
    1
⊢ 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
have rw₄ : Eq.{u_1 + 1} (α := (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).SplittingField) 1
  1
Tactic: rw [div_pow, ← map_pow, hb, σ.commutes, div_self ha']