mathlib3

8a8470cc - feat(data/finset/prod): `finset.diag` and `finset.off_diag` lemmas (#16808)

feat(data/finset/prod): `finset.diag` and `finset.off_diag` lemmas (#16808) Additional lemmas for `diag` and `off_diag` including `finset.coe_off_diag` to relate `finset.off_diag` to `set.off_diag`. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>