no goals
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ (⋃ (i : ι) (hi : p i), Ico (f i hi) a) = Iio a ↔ ∀ (x : α), x < a → ∃ i hi, f i hi ≤ x
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]