mathlib

4676b31f - feat(data/sym2): add the universal property, and make `sym2.is_diag ⟦(x, y)⟧ ↔ x = y` true definitionally (#8358)