-- 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 :
  (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 - Q x * P z) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      W.addZ P Q =
    W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
rw₁ :
  (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 - Q x * P z) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)) =
    W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
rw₂ :
  (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 - Q x * P z) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)) =
    W.toAffine.addX (P x / P z) (Q x / Q z) ((P y * Q z - Q y * P z) / (P x * Q z - Q x * P z))
rw₃ rw₄ :
  (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 - Q x * P z) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q 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 - Q x * P z) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z))
⊢ W.addX P Q / W.addZ P Q =
    W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

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

Premises used: Iff.mpr, _private.0.WeierstrassCurve.Projective.toAffine_addX_of_ne, sub_ne_zero, _private.0.WeierstrassCurve.Projective.toAffine_slope_of_ne, WeierstrassCurve.Projective.addZ_eq, WeierstrassCurve.Projective.addX_eq