feat(measure_theory/outer_measure): golf, add lemmas (#6664)

* `Union_of_tendsto_zero`, `Union_nat_of_monotone_of_tsum_ne_top`, `of_function_union_of_separated`:
  supporting lemmas for the upcoming definition of the Hausdorff
  measure (and more generally metric outer measures).
* `ext_nonempty`, `smul_supr`, `map_sup`, `map_supr`, `comap_supr`,
  `restrict_univ`, `restrict_empty`, `restrict_supr`, `map_comap`,
  `map_comap_le`, `map_comap_of_surjective`, `restrict_le_self`,
  `map_le_restrict_range`, `le_comap_map`, `comap_map`, `comap_top`,
  `top_apply'`, `map_top`, `map_top_of_surjective`: new API lemmas
  about `map`/`comap`/`restrict` and `sup`/`supr`/`top`;
* `is_greatest_of_function`, `of_function_eq_Sup`,
`comap_of_function`, `map_of_function_le`, `map_of_function`,
restrict_of_function`, `smul_of_function`: new lemmas about
`of_function`;
* `Inf_apply'`: a version of `Inf_apply` that assumes that another set
is nonempty;
* `infi_apply`, `infi_apply'`, `binfi_apply`, `binfi_apply'`,
`map_infi_le`, `comap_infi`, `map_infi`, `map_infi_comap`,
`map_binfi_comap`, `restrict_infi_restrict`, `restrict_infi`,
`restrict_binfi`: new lemmas about `map`/`comap`/`restrict` and
`Inf`/`infi`;
* `extend_congr`: `infi_congr_Prop` specialized for `extend`; why this
is not a `congr` lemma?
* `le_induced_outer_measure`: `le_of_function` for
`induced_outer_measure`;
* `trim_le_trim` → `trim_mono`: rename, use `monotone`;
* `exists_measurable_superset_forall_eq_trim`: a version of
`exists_measurable_superset_eq_trim` that works for countable families
of measures;
* `trim_binop`, `trim_op`: new helper lemmas to golf `trim_add` etc;
* `trim_sup`, `trim_supr`: new lemmas about `trim`.
* `map_mono`, `comap_mono`, `mono''`, `restrict_mono`, `trim_mono`:
`@[mono]` lemmas.