-- 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
hy : P y * Q z ≠ W.negY Q * P z
rw :
  (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                  (P y - W.negY P) -
              W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
          (P y - W.negY P) /
        P z /
      W.dblZ P =
    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 (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                  (P y - W.negY P) -
              W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
          (P y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    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 (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                  (P y - W.negY P) -
              W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
          (P y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    W.toAffine.addX (P x / P z) (Q x / Q z)
      (HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P))
rw₃ :
  (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                  (P y - W.negY P) -
              W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
          (P y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    W.toAffine.addX (P x / P z) (P x / P z)
      (HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P))
rw₄ rw₅ :
  (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                  (P y - W.negY P) -
              W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
          (P y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                  (P y - W.negY P) -
              W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
          (P y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3)
⊢ W.dblX P / W.dblZ P =
    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 [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]

Premises used: Iff.mpr, _private.0.WeierstrassCurve.Projective.toAffine_slope_of_eq, sub_ne_zero, _private.0.WeierstrassCurve.Projective.toAffine_addX_of_eq, WeierstrassCurve.Projective.X_eq_iff, WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne', Iff.mp, WeierstrassCurve.Projective.dblX_eq, WeierstrassCurve.Projective.dblZ