no goals
F : Type ?u.343154
α : Type u_1
β : Type ?u.343160
γ : Type ?u.343163
ι : Type ?u.343166
κ : Type ?u.343169
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x a : α
⊢ max' {a} (_ : Finset.Nonempty {a}) = a
simp [max']