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), Ioc a (f i hi)) = Ioi a ↔ ∀ (x : α), a < x → ∃ i hi, x ≤ f i hi
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]