no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : Set.Finite s
x : α
hx : x ∈ s
⊢ ∃ a, a ∈ s ∧ ∀ (b : α), b ∈ s → f a ≤ f b
simpa only [exists_prop, Finite.mem_toFinset] using
  h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩