no goals
α : Type u_2
β : Type ?u.18395
inst✝ : EDist α
x y : α
s✝ t : Set α
ι : Type u_1
o : Option ι
s : ι → Set α
⊢ einfsep (⋃ (i : ι) (_ : i ∈ o), s i) = ⨅ (i : ι) (_ : i ∈ o), einfsep (s i)
cases o <;> simp