feat(data/fintype): golf, move and dualise proof (#7126)

This PR moves `fintype.exists_max` higher up in the import tree, and golfs it, and adds the dual version, `fintype.exists_min`. The name and statement are unchanged.

src/data/fintype/basic.lean

@@ -169,6 +169,16 @@ instance decidable_right_inverse_fintype [decidable_eq β] [fintype β] (f : α
   decidable (function.left_inverse f g) :=
 show decidable (∀ x, f (g x) = x), by apply_instance
 
+lemma exists_max [fintype α] [nonempty α]
+  {β : Type*} [linear_order β] (f : α → β) :
+  ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
+by simpa using exists_max_image univ f univ_nonempty
+
+lemma exists_min [fintype α] [nonempty α]
+  {β : Type*} [linear_order β] (f : α → β) :
+  ∃ x₀ : α, ∀ x, f x₀ ≤ f x :=
+by simpa using exists_min_image univ f univ_nonempty
+
 /-- Construct a proof of `fintype α` from a universal multiset -/
 def of_multiset [decidable_eq α] (s : multiset α)
   (H : ∀ x : α, x ∈ s) : fintype α :=

src/data/set/finite.lean

@@ -767,11 +767,3 @@ protected lemma bdd_below [semilattice_inf α] [nonempty α] (s : finset α) :
 s.finite_to_set.bdd_below
 
 end finset
-
-lemma fintype.exists_max [fintype α] [nonempty α]
-  {β : Type*} [linear_order β] (f : α → β) :
-  ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
-begin
-  rcases set.finite_univ.exists_maximal_wrt f _ univ_nonempty with ⟨x, _, hx⟩,
-  exact ⟨x, λ y, (le_total (f x) (f y)).elim (λ h, ge_of_eq $ hx _ trivial h) id⟩
-end