{R : Type r} →
  {S : Type s} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (W' : WeierstrassCurve.Affine R) →
          (f : R →+* S) → W'.CoordinateRing →+* (WeierstrassCurve.map W' f).toAffine.CoordinateRing