-- 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
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw :
  (-W.dblU P * (W.dblX P - P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) + P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (W.dblZ P) 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₁ :
  (-W.dblU P *
          (HPow.hPow (β := ℕ) (W.dblU P) 2 - W.a₁ * W.dblU P * 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 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (W.dblZ P) 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₂ :
  (-W.dblU P *
          (HPow.hPow (β := ℕ) (W.dblU P) 2 - W.a₁ * W.dblU P * 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 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (W.dblZ P) 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.dblU P / W.dblZ P)
rw₃ :
  (-W.dblU P *
          (HPow.hPow (β := ℕ) (W.dblU P) 2 - W.a₁ * W.dblU P * 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 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 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.dblU P / (P z * (P y - W.negY P)))
rw₄ :
  (-W.dblU P *
          (HPow.hPow (β := ℕ) (W.dblU P) 2 - W.a₁ * W.dblU P * 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 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 3 =
    W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (P x / HPow.hPow (β := ℕ) (P z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (-W.dblU P / (P z * (P y - W.negY P)))
rw₅ rw₆ :
  (-W.dblU P *
          (HPow.hPow (β := ℕ) (W.dblU P) 2 - W.a₁ * W.dblU P * 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 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 3 =
    (-W.dblU P *
          (HPow.hPow (β := ℕ) (W.dblU P) 2 - W.a₁ * W.dblU P * 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 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 3
⊢ W.negDblY P / HPow.hPow (β := ℕ) (W.dblZ P) 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 [negDblY, dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]

Premises used: Iff.mpr, sub_ne_zero, WeierstrassCurve.Jacobian.X_eq_iff, WeierstrassCurve.Jacobian.dblZ, WeierstrassCurve.Jacobian.dblX, _private.0.WeierstrassCurve.Jacobian.toAffine_negAddY_of_eq, Iff.mp, WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne', WeierstrassCurve.Jacobian.negDblY, _private.0.WeierstrassCurve.Jacobian.toAffine_slope_of_eq