no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c, c ∈ s ∧ b < c
simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]