no goals
ι : Sort u
α : Type v
β : Type w
inst✝¹ : LinearOrder α
s : Set α
a : α
f✝ : ι → α
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
has_least_elem : (⨅ (i : ι), f i) ∈ range f
⊢ (⋃ (i : ι), Ici (f i)) = Ici (⨅ (i : ι), f i)
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
  iUnion_exists, iUnion_iUnion_eq']