no goals
ι : Type ?u.1024328
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam (↑h ⁻¹' s) = Metric.diam s
rw [← image_symm, diam_image]