Push_neg port

Stream: mathlib4

[Alice Laroche]

I made a pull request with a port of the push_neg tactic
https://github.com/leanprover-community/mathlib4/pull/193

[Kevin Buzzard]

Thank you!

[Arthur Paulino]

Alice ended up closing the PR (mathlib4#193). Can someone help me understand why?

• Was the approach inadequate in a more fundamental level? or
• The approach was correct but had some missing cases?

[Gabriel Ebner]

See my comments. I think fundamentally it's the approach that we want. But it constructs congruence lemmas incorrectly, so it will fail on decide, ite, etc. It would also be good to use the Simp.Result API because that simplifies the code quite a bit.