simp [dweierstrass_dx]
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
P : R × R
⊢ dweierstrass_dx (map f e) (Prod.map (↑f) (↑f) P) = ↑f (dweierstrass_dx e P)
no goals