case intro.intro
F : Type ?u.313391
α : Type u_1
β : Type ?u.313397
γ : Type ?u.313400
ι : Type ?u.313403
κ : Type ?u.313406
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : b ∈ sup s some
right✝ : a ≤ b
⊢ ∃ b, Finset.max s = ↑b
F : Type ?u.313391
α : Type u_1
β : Type ?u.313397
γ : Type ?u.313400
ι : Type ?u.313403
κ : Type ?u.313406
inst✝ : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ b, Finset.max s = ↑b
obtain ⟨b, h, _⟩ := le_sup (α := WithBot α) h _ rfl
no goals
case intro.intro
F : Type ?u.313391
α : Type u_1
β : Type ?u.313397
γ : Type ?u.313400
ι : Type ?u.313403
κ : Type ?u.313406
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : b ∈ sup s some
right✝ : a ≤ b
⊢ ∃ b, Finset.max s = ↑b
exact ⟨b, h⟩