Kevin Buzzard (Jul 04 2019 at 17:14):
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
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 (Jul 04 2019 at 17:20):
Johan Commelin (Jul 04 2019 at 17:21):
That's imported by almost everything else, and it seems a fitting place.
Last updated: May 13 2021 at 05:21 UTC