-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
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))
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))
rw₃ 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 =
    ((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.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))

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]

Premises used: WeierstrassCurve.Jacobian.negAddY_eq, WeierstrassCurve.Jacobian.addX_eq', _private.0.WeierstrassCurve.Jacobian.toAffine_negAddY_of_ne, WeierstrassCurve.Jacobian.addZ_ne_zero_of_X_ne, _private.0.WeierstrassCurve.Jacobian.toAffine_slope_of_ne