∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} {hP : W.NonsingularLift ⟦P⟧}
  (hPz : P 2 ≠ 0), { point := ⟦P⟧, nonsingular := hP }.toAffineLift = WeierstrassCurve.Affine.Point.some ⋯