no goals
α : Type u_1
β : Type ?u.58938
γ : Type ?u.58941
ι : Sort ?u.58944
κ : ι → Sort ?u.58949
inst✝ : LE α
S : Set (UpperSet α)
s t : UpperSet α
a : α
⊢ (∃ i j, a ∈ ↑i) ↔ ∃ s, s ∈ S ∧ a ∈ s
simp only [exists_prop, SetLike.mem_coe]