-- 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)
r₁ r₂ : S
h_1 : IsNilpotent (r₁ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
h_2 : IsNilpotent (r₂ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
hr₁ : IsNilpotent (r₁ - x)
hr₁' : Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
hr₂ : IsNilpotent (r₂ - x)
hr₂' : Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) * (r₂ - r₁) +
      u * HPow.hPow (β := ℕ) (r₂ - r₁) 2
this :
  IsUnit
    (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S) (u * (r₂ - r₁)))
rwa :
  ∀
    (hu :
      eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
        eval r₁ (map (algebraMap R S) P) +
            eval r₁ (map (algebraMap R S) ((derivative : (a : R[X]) → R[X]) P)) * (r₂ - r₁) +
          u * HPow.hPow (β := ℕ) (r₂ - r₁) 2)
    (this :
      IsUnit
        (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
          (u * (r₂ - r₁)))),
    r₁ = r₂
rwa₁ :
  ∀
    (hu :
      (aeval (r₁ + (r₂ - r₁)) : (a : R[X]) → S) P =
        eval r₁ (map (algebraMap R S) P) +
            eval r₁ (map (algebraMap R S) ((derivative : (a : R[X]) → R[X]) P)) * (r₂ - r₁) +
          u * HPow.hPow (β := ℕ) (r₂ - r₁) 2)
    (this :
      IsUnit
        (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
          (u * (r₂ - r₁)))),
    r₁ = r₂
rwa₂ :
  ∀
    (hu :
      (aeval (r₁ + (r₂ - r₁)) : (a : R[X]) → S) P =
        HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) P : S)
            (eval r₁ (map (algebraMap R S) ((derivative : (a : R[X]) → R[X]) P)) * (r₂ - r₁)) +
          u * HPow.hPow (β := ℕ) (r₂ - r₁) 2)
    (this :
      IsUnit
        (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
          (u * (r₂ - r₁)))),
    r₁ = r₂
rwa₃ :
  ∀
    (hu :
      (aeval (r₁ + (r₂ - r₁)) : (a : R[X]) → S) P =
        HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) P : S)
            (HMul.hMul (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
              (r₂ - r₁)) +
          u * HPow.hPow (β := ℕ) (r₂ - r₁) 2)
    (this :
      IsUnit
        (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
          (u * (r₂ - r₁)))),
    r₁ = r₂
rwa₄ :
  ∀
    (hu :
      (aeval r₂ : (a : R[X]) → S) P =
        HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) P : S)
            (HMul.hMul (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
              (r₂ - r₁)) +
          u * HPow.hPow (β := ℕ) (r₂ - r₁) 2)
    (this :
      IsUnit
        (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
          (u * (r₂ - r₁)))),
    r₁ = r₂
⊢ r₁ = r₂
have rwa₅ : ∀
  (hu :
    0 =
      HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) P : S)
          (HMul.hMul (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S) (r₂ - r₁)) +
        u * HPow.hPow (β := ℕ) (r₂ - r₁) 2)
  (this :
    IsUnit
      (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
        (u * (r₂ - r₁)))),
  r₁ = r₂
Tactic: rwa [derivative_map, eval_map_algebraMap, eval_map_algebraMap, eval_map_algebraMap,
        add_sub_cancel, hr₂', hr₁', zero_add, pow_two, ← mul_assoc, ← add_mul, eq_comm,
        this.mul_right_eq_zero, sub_eq_zero, eq_comm] at hu
Cleared hypotheses: hu, this