simp only [lt_iff_exists_forall_lt]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ { ofColex := s } < { ofColex := t } ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)