mathlib

f157a372 - chore(logic/basic): fixup `eq_or_ne` (#7865)