-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z ≠ Q x * P z
rw :
  ((P y * Q z - Q y * P z) *
            (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                  P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) +
          P y * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      W.addZ P Q =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
rw₁ :
  ((P y * Q z - Q y * P z) *
            (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                  P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) +
          P y * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)) =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
rw₂ :
  ((P y * Q z - Q y * P z) *
            (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                  P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) +
          P y * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)) =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z) ((P y * Q z - Q y * P z) / (P x * Q z - Q x * P z))
rw₃ rw₄ :
  ((P y * Q z - Q y * P z) *
            (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                  P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) +
          P y * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)) =
    ((P y * Q z - Q y * P z) *
            (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                  P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
                Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) +
          P y * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z))
⊢ W.negAddY P Q / W.addZ P Q =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
rw [negAddY_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| sub_ne_zero.mpr hx]

Premises used: Iff.mpr, sub_ne_zero, _private.0.WeierstrassCurve.Projective.toAffine_slope_of_ne, WeierstrassCurve.Projective.addZ_eq, WeierstrassCurve.Projective.negAddY_eq, _private.0.WeierstrassCurve.Projective.toAffine_negAddY_of_ne