mathlib

37bf8a2e - chore(topology/separation): Extract `set` product lemma (#14958)

chore(topology/separation): Extract `set` product lemma (#14958) Move `prod_subset_compl_diagonal_iff_disjoint` to `data.set.prod`, where it belongs. Delete `diagonal_eq_range_diagonal_map` because it duplicates `set.diagonal_eq_range`. Move `set.disjoint_left`/`set.disjoint_right` to `data.set.basic` to avoid an import cycle. Make variable semi-implicit in the RHS of `disjoint_left` and `disjoint_right`.