feat(data/finset): max_of_ne_empty, min_of_ne_empty

data/finset.lean

@@ -1237,11 +1237,12 @@ max_singleton
 theorem max_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.max :=
 (@le_sup (with_bot α) _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
 
+theorem max_of_ne_empty {s : finset α} (h : s ≠ ∅) : ∃ a, a ∈ s.max :=
+let ⟨a, ha⟩ := exists_mem_of_ne_empty h in max_of_mem ha
+
 theorem max_eq_none {s : finset α} : s.max = none ↔ s = ∅ :=
-⟨λ h, by_contradiction
-  (λ hs, let ⟨a, ha⟩ := exists_mem_of_ne_empty hs in
-  let ⟨b, hb⟩ := max_of_mem ha in
-  by simpa [h] using hb),
+⟨λ h, by_contradiction $
+  λ hs, let ⟨a, ha⟩ := max_of_ne_empty hs in by simpa [h] using ha,
 λ h, h.symm ▸ max_empty⟩
 
 theorem mem_of_max {s : finset α} : ∀ {a : α}, a ∈ s.max → a ∈ s :=
@@ -1278,11 +1279,12 @@ by simp [finset.min, option.lift_or_get]
 theorem min_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.min :=
 (@inf_le (with_top α) _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
 
+theorem min_of_ne_empty {s : finset α} (h : s ≠ ∅) : ∃ a, a ∈ s.min :=
+let ⟨a, ha⟩ := exists_mem_of_ne_empty h in min_of_mem ha
+
 theorem min_eq_none {s : finset α} : s.min = none ↔ s = ∅ :=
-⟨λ h, by_contradiction
-  (λ hs, let ⟨a, ha⟩ := exists_mem_of_ne_empty hs in
-  let ⟨b, hb⟩ := min_of_mem ha in
-  by simpa [h] using hb),
+⟨λ h, by_contradiction $
+  λ hs, let ⟨a, ha⟩ := min_of_ne_empty hs in by simpa [h] using ha,
 λ h, h.symm ▸ min_empty⟩
 
 theorem mem_of_min {s : finset α} : ∀ {a : α}, a ∈ s.min → a ∈ s :=