-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
pos :
  Eq (α := PointClass F) ⟦W.add P Q⟧
    ⟦![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)),
        W.toAffine.addY (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)),
        1]⟧
pos₁ :
  Eq (α := PointClass F)
    ⟦W.dblZ P •
        ![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)),
          W.toAffine.addY (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)),
          1]⟧
    ⟦![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)),
        W.toAffine.addY (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)),
        1]⟧
pos₂ pos₃ :
  Eq (α := PointClass F)
    ⟦![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)),
        W.toAffine.addY (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)),
        1]⟧
    ⟦![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)),
        W.toAffine.addY (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)),
        1]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧)
    ⟦![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)),
        W.toAffine.addY (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)),
        1]⟧

Tactic:
rw [addMap_eq, add_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx,
      smul_eq _ <| isUnit_dblZ_of_Y_ne' hP hQ hPz hx <| not_and.mp hxy hx]

Premises used: WeierstrassCurve.Jacobian.add_of_Y_ne', WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne', Iff.mp, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.addMap_eq, not_and