mathlib

2c2d515a - refactor(data/list/min_max): Generalise `list.argmin`/`list.argmax` to preorders (#13221)

refactor(data/list/min_max): Generalise `list.argmin`/`list.argmax` to preorders (#13221) This PR generalises the contents of the `data/list/min_max` file from a `linear_order` down to a `preorder` with decidable `<`. Note that for this to work out, I have had to change the structure of the auxiliary function `argmax₂` to now mean `option.cases_on a (some b) (λ c, if f c < f b then some b else some c)`. This is because in the case of a preorder, `argmax₂` would perform the swap in the absence of the `≤` relation, which would result in a semi-random shuffle that doesn't look very `maximal`. Co-authored-by: YaelDillies <yael.dillies@gmail.com>