feat(Data/Finset/Max): min'_pair, max'_pair (#29415)

Add the lemmas:

```lean
lemma min'_pair (a b : α) : min' {a, b} (insert_nonempty _ _) = min a b := by
```

```lean
lemma max'_pair (a b : α) : max' {a, b} (insert_nonempty _ _) = max a b := by
```

and corresponding `min_pair` and `max_pair`. So that the primed lemmas can be proved by `simp`, like the unprimed ones, make `min'_insert` and `max'_insert` into `simp` lemmas, and swap the arguments to `min` and `max` on their RHS, also corresponding more closely to the unprimed lemmas `min_insert` and `max_insert`.

Author: jsm28

Mathlib/Data/Finset/Max.lean

@@ -49,6 +49,10 @@ theorem max_singleton {a : α} : Finset.max {a} = (a : WithBot α) := by
   rw [← insert_empty_eq]
   exact max_insert
 
+lemma max_pair (a b : α) :
+    Finset.max {a, b} = max (↑a) (↑b) := by
+  simp
+
 theorem max_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.max = b := by
   obtain ⟨b, h, _⟩ := le_sup (α := WithBot α) h _ rfl
   exact ⟨b, h⟩
@@ -132,6 +136,10 @@ theorem min_singleton {a : α} : Finset.min {a} = (a : WithTop α) := by
   rw [← insert_empty_eq]
   exact min_insert
 
+lemma min_pair (a b : α) :
+    Finset.min {a, b} = min (↑a) (↑b) := by
+  simp
+
 theorem min_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.min = b := by
   obtain ⟨b, h, _⟩ := inf_le (α := WithTop α) h _ rfl
   exact ⟨b, h⟩
@@ -312,18 +320,26 @@ theorem min'_subset {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) :
     t.min' (H.mono hst) ≤ s.min' H :=
   min'_le _ _ (hst (s.min'_mem H))
 
-theorem max'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
-    (insert a s).max' (s.insert_nonempty a) = max (s.max' H) a :=
+@[simp] theorem max'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
+    (insert a s).max' (s.insert_nonempty a) = max a (s.max' H) :=
   (isGreatest_max' _ _).unique <| by
-    rw [coe_insert, max_comm]
+    rw [coe_insert]
     exact (isGreatest_max' _ _).insert _
 
-theorem min'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
-    (insert a s).min' (s.insert_nonempty a) = min (s.min' H) a :=
+@[simp] theorem min'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
+    (insert a s).min' (s.insert_nonempty a) = min a (s.min' H) :=
   (isLeast_min' _ _).unique <| by
-    rw [coe_insert, min_comm]
+    rw [coe_insert]
     exact (isLeast_min' _ _).insert _
 
+lemma min'_pair (a b : α) :
+    min' {a, b} (insert_nonempty _ _) = min a b := by
+  simp
+
+lemma max'_pair (a b : α) :
+    max' {a, b} (insert_nonempty _ _) = max a b := by
+  simp
+
 theorem lt_max'_of_mem_erase_max' [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.max' H)) :
     a < s.max' H :=
   lt_of_le_of_ne (le_max' _ _ (mem_of_mem_erase ha)) <| ne_of_mem_of_not_mem ha <| notMem_erase _ _