Commit 2025-09-15 15:53 1e81efcd

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

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

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.