no goals
ι : Type ?u.688882
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ↑h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (↑(IsometryEquiv.symm h) x) r
rw [← h.isometry.preimage_emetric_closedBall (h.symm x) r, h.apply_symm_apply]