α : Type u_1
β : Type ?u.82988
γ : Type ?u.82991
ι : Sort ?u.82994
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ (b : α), b ∈ s → b ≤ a
⊢ sSup s ≤ a
α : Type u_1
β : Type ?u.82988
γ : Type ?u.82991
ι : Sort ?u.82994
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a < sSup s
⊢ ∃ b, b ∈ s ∧ a < b
contrapose! h
no goals
α : Type u_1
β : Type ?u.82988
γ : Type ?u.82991
ι : Sort ?u.82994
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ (b : α), b ∈ s → b ≤ a
⊢ sSup s ≤ a
exact csSup_le' h