no goals
ι : Type ?u.725615
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ↑h '' EMetric.ball x r = EMetric.ball (↑h x) r
rw [← h.preimage_symm, h.symm.preimage_emetric_ball, symm_symm]