no goals
X : Type u_2
inst✝ : EMetricSpace X
s✝ t✝ : Set X
x y : X
ι : Type u_1
I : Set ι
hI : Set.Finite I
s : Set X
t : ι → Set X
⊢ IsMetricSeparated s (⋃ (i : ι) (_ : i ∈ I), t i) ↔ ∀ (i : ι), i ∈ I → IsMetricSeparated s (t i)
simpa only [@comm _ _ s] using finite_iUnion_left_iff hI