no goals
F : Type ?u.336329
α : Type u_1
β : Type ?u.336335
γ : Type ?u.336338
ι : Type ?u.336341
κ : Type ?u.336344
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x a : α
⊢ min' {a} (_ : Finset.Nonempty {a}) = a
simp [min']