-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
rw :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    0
rw₁ :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
rw₂ :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
        (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
        (HPow.hPow (α := K[X]) X n) -
      eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
        (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
        ((C : (a : K) → K[X]) a)
rw₃ :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
        (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
        (HPow.hPow (α := K[X]) X n))
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
rw₄ :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
          (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) X ^
        n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n =
    (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
      a
have rw₅ : HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
    ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
        a :
      AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
    ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
        a :
      AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
Tactic: rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]