F : Type ?u.408857
α : Type u_1
β : Type ?u.408863
γ : Type ?u.408866
ι : Type ?u.408869
κ : Type ?u.408872
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : Finset.Nonempty s
⊢ i ∈ ↑s
F : Type ?u.408857
α : Type u_1
β : Type ?u.408863
γ : Type ?u.408866
ι : Type ?u.408869
κ : Type ?u.408872
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : Finset.Nonempty s
⊢ i ∈ s
rw [← mem_coe]
no goals
F : Type ?u.408857
α : Type u_1
β : Type ?u.408863
γ : Type ?u.408866
ι : Type ?u.408869
κ : Type ?u.408872
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : Finset.Nonempty s
⊢ i ∈ ↑s
exact ((is_glb_iff_is_least i s hs).mp his).1