∀ {F : Type u_1} [inst : Field F] (W : WeierstrassCurve.Projective F) [DecidableEq F],
  Function.LeftInverse WeierstrassCurve.Projective.Point.fromAffine WeierstrassCurve.Projective.Point.toAffineLift