Commit 2025-09-23 03:07 79b52d2c

feat: extensible push and pull tactics (#21965) This PR defines the push and pull tactics, and makes push_neg a macro for push Not. The tactics are also available in conv mode. For tagging, there is only the @[push] attribute, which adds the reverse rewrite for the pull tactic when relevant. In the future, we may also need a separate @[pull X] attribute for pulling X. Thanks to this change, we will be able to make push_neg into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import LinearOrder/PartialOrder. This will be especially useful when we get the @[to_dual] attribute. This work originally started in #21769. There is now the follow up PR #29000 which adds push tags and tests for them. The @[push] attribute is defined in Mathlib.Tactic.Push.Attr and the main implementation of push and pull is in Mathlib.Tactic.Push. Some proofs need to be fixed because the new simp-based push_neg can see through more reducible definitions. Zulip conversation: [#mathlib4 > I made an extensible `push` tactic generalizing `push_neg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60) closes #21841