no goals
ι : Type ?u.1172241
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : α
r : ℝ
⊢ ↑h '' Metric.sphere x r = Metric.sphere (↑h x) r
rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]