-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
succ :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
have succ₁ : HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
  HPow.hPow (β := ℕ)
    (HMul.hMul (α := S) (β := S)
      (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
      ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
    2
Tactic: refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)