symmetry

Stream: general

[Kevin Buzzard]

The symmetry tactic won't turn a ≠ b into b ≠ a (at least it won't for my home-grown nats). This can be fixed with

attribute [symm] ne.symm

Unfortunately ne.symm is in core so it's not so easy to tag it with this attribute. Is there a place in mathlib where this line could go?

[Johan Commelin]

data/logic.lean?

[Johan Commelin]

That's imported by almost everything else, and it seems a fitting place.