case intro.intro
F : Type ?u.324381
α : Type u_1
β : Type ?u.324387
γ : Type ?u.324390
ι : Type ?u.324393
κ : Type ?u.324396
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : b ∈ inf s some
right✝ : b ≤ a
⊢ ∃ b, Finset.min s = ↑b
F : Type ?u.324381
α : Type u_1
β : Type ?u.324387
γ : Type ?u.324390
ι : Type ?u.324393
κ : Type ?u.324396
inst✝ : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ b, Finset.min s = ↑b
obtain ⟨b, h, _⟩ := inf_le (α := WithTop α) h _ rfl
no goals
case intro.intro
F : Type ?u.324381
α : Type u_1
β : Type ?u.324387
γ : Type ?u.324390
ι : Type ?u.324393
κ : Type ?u.324396
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : b ∈ inf s some
right✝ : b ≤ a
⊢ ∃ b, Finset.min s = ↑b
exact ⟨b, h⟩