-- 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
hZ : IsUnit (W.addZ P Q)
erw :
  ![W.addX P Q, W.addY P Q, W.addZ 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)),
        W.toAffine.addY (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)),
        1]
erw₁ :
  ![W.addX P Q, W.addY P Q, W.addZ 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)),
            W.toAffine.addY (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)),
            1]
          x,
      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)),
            W.toAffine.addY (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)),
            1]
          y,
      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)),
            W.toAffine.addY (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)),
            1]
          z]
erw₂ :
  ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (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)),
            1]
          x,
      W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (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)),
            1]
          y,
      W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (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)),
            1]
          z]
erw₃ :
  ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addX P Q,
      W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (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)),
            1]
          y,
      W.addZ P Q *
        ![W.addX P Q / W.addZ P Q,
            W.toAffine.addY (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)),
            1]
          z]
erw₄ :
  ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addX P Q, W.addZ P Q * ![W.addX P Q / W.addZ P Q, W.addY P Q / W.addZ P Q, 1] y,
      W.addZ P Q * ![W.addX P Q / W.addZ P Q, W.addY P Q / W.addZ P Q, 1] z]
erw₅ :
  ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addX P Q, W.addY P Q, W.addZ P Q * ![W.addX P Q / W.addZ P Q, W.addY P Q / W.addZ P Q, 1] z]
erw₆ erw₇ : ![W.addX P Q, W.addY P Q, W.addZ P Q] = ![W.addX P Q, W.addY P Q, W.addZ P Q]
⊢ W.addXYZ 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)),
        W.toAffine.addY (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)),
        1]

Tactic:
erw [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
    ← addY_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, mul_one]

Premises used: IsUnit.mul_div_cancel, WeierstrassCurve.Projective.addY_of_Z_ne_zero, WeierstrassCurve.Projective.smul_fin3, mul_one, WeierstrassCurve.Projective.addXYZ, WeierstrassCurve.Projective.addX_of_Z_ne_zero