refactor(order/well_founded_set): golf, review API (#11303)
## New lemmas
### About `set.well_founded_on`
- `set.well_founded_on.mono`, `set.well_founded_on.mono_set`;
- `set.well_founded_on.union`, `set.well_founded_on_union`,
`finset.well_founded_on`, `set.finite.well_founded_on`,
`set.subsingleton.well_founded_on`, `set.well_founded_on_empty`,
`set.well_founded_on_singleton`, `set.well_founded_on_insert`,
`set.well_founded_on.insert`;
### About `set.is_wf`
- `set.is_wf_union`;
- `set.finite.is_wf`, `finset.is_wf`, `set.is_wf_empty`,
`set.is_wf_singleton`, `set.subsingleton.is_wf`, `set.is_wf_insert`,
`set.is_wf.insert`;
- `finset.is_wf_bUnion`
### About `set.partially_well_ordered_on`
- `set.partially_well_ordered_on.union`,
`set.partially_well_ordered_on_union`;
- `set.finite.partially_well_ordered_on`,
`finset.partially_well_ordered_on`,
`set.partially_well_ordered_on_empty`,
`set.partially_well_ordered_on_singleton`,
`set.partially_well_ordered_on_insert` (an `iff`),
`set.partially_well_ordered_on.insert`,
`set.subsingleton.partially_well_ordered_on`;
### About `set.is_pwo`
- `set.is_pwo.image_of_monotone_on`, `set.is_pwo_union`;
- `finset.is_pwo`, `set.is_pwo_insert`;
- `finset.is_pwo_bUnion`;
## Other API changes
- Definitions lemmas now use `∀ n, f n ∈ s` instead of `range f ⊆ s`.
- Many lemmas now use weaker TC assumptions (e.g., `preorder` instead
of `partial_order`).
- `set.is_wf_iff_no_descending_seq` now uses
`(f : ℕ → α) (hf : strict_anti f)` instead of
`f : order_dual ℕ ↪o α`.
- The order of binders in the `hf` argument of
`set.partially_well_ordered_on.image_of_monotone_on` was changed to
match `monotone_on`.
- `set.is_pwo.prod` now allows sets from different types.
- `finset.is_wf_sup` and `finset.is_pwo_sup` are now `iff`s
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
