no goals
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
f : ι → α
a : α
⊢ (⋃ (i : ι), Ioc a (f i)) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]