mathlib
1fecd52f - fix(tactic/push_neg): fully simplify expressions not named `h` (#6297)

Commit
4 years ago
fix(tactic/push_neg): fully simplify expressions not named `h` (#6297) A final pass of `push_neg` is intended to turn `¬ a = b` into `a ≠ b`. Unfortunately, when you use `push_neg at ...`, this is applied to the hypothesis literally named `h`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60push_neg.60.20behaviour.20depends.20on.20variable.20name) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading