-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
            (W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 -
              P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) +
          P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (addZ P Q) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 3 /
      HPow.hPow (β := ℕ) (addZ P Q) 3 =
    W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
rw₁ :
  ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
            (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
                      W.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z *
                        addZ P Q -
                    W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
                  P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
                Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
              P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) +
          P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (addZ P Q) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 3 /
      HPow.hPow (β := ℕ) (addZ P Q) 3 =
    W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
⊢ W.negAddY P Q / HPow.hPow (β := ℕ) (addZ P Q) 3 =
    W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
have rw₂ : ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
          (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
                    W.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z *
                      addZ P Q -
                  W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
                P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
              Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
            P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) +
        P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (addZ P Q) 3) /
      HPow.hPow (β := ℕ) (P z * Q z) 3 /
    HPow.hPow (β := ℕ) (addZ P Q) 3 =
  W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
    (P y / HPow.hPow (β := ℕ) (P z) 3)
    ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z * addZ P Q))
Tactic: rw [negAddY_eq hPz hQz, addX_eq' hP hQ, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]