∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  {P : Fin 3 → R}, W'.Equation P → (WeierstrassCurve.map W' f).toProjective.Equation (⇑f ∘ P)