-- 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
this :
  IsUnit.{u_2} (M := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
h₁ :
  HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) (map (algebraMap R S) ((derivative : (a : R[X]) → R[X]) 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)) =
    0
h₂ :
  HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (HMul.hMul (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
        (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))) =
    0
h₃ :
  HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : 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)) =
    0
⊢ 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)) =
    0
have h₄ : HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
    (HMul.hMul (β := S)
      (-HMul.hMul (α := S) (β := S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : 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)) =
  0
Tactic: rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]