∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x : R),
  WeierstrassCurve.Affine.CoordinateRing.XClass W' x =
    (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.C (Polynomial.X - Polynomial.C x))