no goals
α : Type u_1
β : Type ?u.24202
γ : Type ?u.24205
ι : Sort ?u.24208
κ : ι → Sort ?u.24213
inst✝ : PartialOrder α
s : Set α
a : α
⊢ (∀ ⦃b : α⦄, a ≤ b → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, a < b → a ∈ s → b ∈ s
simp [le_iff_eq_or_lt, or_imp, forall_and]