Symmetric simp #73
Description
See leanprover-community#33363
It feels like instead of having to add these, it might be better if simp could identify equalities and try to match both the equality and its symm. We could potentially even do this for other symmetric relations.