mathlib3

210657c4 - refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'` (#15071)

refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'` (#15071) The predicate `x ≤ y → y = x` is no more convenient than `¬ x < y`. For this reason, we ditch `well_founded.well_founded_iff_has_min'` and `well_founded.well_founded_iff_has_max'` in favor of `well_founded.well_founded_iff_has_min` (or in some cases, just `well_founded.has_min`. We also remove the misplaced lemma `well_founded.eq_iff_not_lt_of_le`, and we golf the theorems that used the removed theorems. The lemma `well_founded.well_founded_iff_has_min` has a misleading name when applied on `well_founded (>)`, and mildly screws over dot notation and rewriting by virtue of using `>`, but a future refactor will fix this.