α : Type u_1
β : Type ?u.8944
γ : Type ?u.8947
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ max' s h ∈ s
α : Type u_1
β : Type ?u.8944
γ : Type ?u.8947
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ sSup ↑s ∈ s
rw [h.cSup_eq_max']
no goals
α : Type u_1
β : Type ?u.8944
γ : Type ?u.8947
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ max' s h ∈ s
exact s.max'_mem _