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