chore(*): improve some definitional equalities (#15083)
* add `set.mem_diagonal_iff`, move `simp` from `set.mem_diagonal`;
* add `@[simp]` to `set.prod_subset_compl_diagonal_iff_disjoint`;
* redefine `sum.map` in terms of `sum.elim`, add `sum.map_inl` and `sum.map_inr`;
* redefine `sum.swap` in terms of `sum.elim`, add `sum.swap_inl` and `sum.swap_inr`;
* use `lift_rel_swap_iff` to prove `swap_le_swap` and `swap_lt_swap`;
* redefine `equiv.sum_prod_distrib` and `equiv.sigma_sum_distrib` in terms of `sum.elim` and `sum.map`;
* add `filter.compl_diagonal_mem_prod`;
* rename `continuous_sum_rec` to `continuous.sum_elim`, use `sum.elim` in the statement;
* add `continuous.sum_map`;
* golf `homeomorph.sum_congr` and `homeomorph.sum_prod_distrib`.
