no goals
ι : Type ?u.1037072
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : β
r : ℝ
⊢ ↑h ⁻¹' Metric.ball x r = Metric.ball (↑(IsometryEquiv.symm h) x) r
rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]