mathlib

c5be877a - feat(tactic/tauto): add support for `¬_ ≠ _` (#16232)

feat(tactic/tauto): add support for `¬_ ≠ _` (#16232) This is an attempt to fix [this issue](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/tauto!.20fails.20on.20ne).