∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (P : W.Point),
  WeierstrassCurve.Affine.Point.toClass P =
    match P with
    | WeierstrassCurve.Affine.Point.zero => 0
    | WeierstrassCurve.Affine.Point.some h =>
      Additive.ofMul (ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h))