no goals
α : Type u
β : Type v
X : Type ?u.286785
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
ι : Type u_1
o : Option ι
s : ι → Set α
⊢ diam (⋃ (i : ι) (_ : i ∈ o), s i) = ⨆ (i : ι) (_ : i ∈ o), diam (s i)
cases o <;> simp