no goals
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
e : F ≃L[𝕜] E
⊢ UniqueDiffOn 𝕜 (↑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]