-- 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 :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (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₁ :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2) (-W.dblU P / W.dblZ P)
rw₂ :
  (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (-W.dblU P / (P z * (P y - W.negY P)))
rw₃ :
  (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (P x / HPow.hPow (β := ℕ) (P z) 2)
      (-W.dblU P / (P z * (P y - W.negY P)))
rw₄ rw₅ :
  (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
    (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2
⊢ W.dblX P / HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (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 [dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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, _private.0.WeierstrassCurve.Jacobian.toAffine_addX_of_eq, WeierstrassCurve.Jacobian.dblX, Iff.mp, WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne', _private.0.WeierstrassCurve.Jacobian.toAffine_slope_of_eq