define attribute before tactic, to reduce import size

Mathlib.lean

@@ -5213,8 +5213,8 @@ import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.ProxyType
 import Mathlib.Tactic.Push
+import Mathlib.Tactic.Push.Attr
 import Mathlib.Tactic.Push.Basic
-import Mathlib.Tactic.Push.Lemmas
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recall

Mathlib/Data/Finite/Defs.lean

@@ -7,7 +7,6 @@ import Mathlib.Data.Set.CoeSort
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Tactic.Set
 import Mathlib.Util.AssertExists
-import Mathlib.Tactic.Push.Basic
 
 /-!
 # Definition of the `Finite` typeclass

Mathlib/Logic/Nontrivial/Defs.lean

@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.TypeStar
-import Mathlib.Tactic.Push.Basic
+import Mathlib.Tactic.Push.Attr
 
 /-!
 # Nontrivial types

Mathlib/Order/Defs/LinearOrder.lean

@@ -8,7 +8,7 @@ import Batteries.Tactic.Trans
 import Mathlib.Data.Ordering.Basic
 import Mathlib.Tactic.ExtendDoc
 import Mathlib.Tactic.Lemma
-import Mathlib.Tactic.Push.Basic
+import Mathlib.Tactic.Push.Attr
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.TypeStar
 import Mathlib.Order.Defs.PartialOrder

Mathlib/Tactic.lean

@@ -206,8 +206,8 @@ import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.ProxyType
 import Mathlib.Tactic.Push
+import Mathlib.Tactic.Push.Attr
 import Mathlib.Tactic.Push.Basic
-import Mathlib.Tactic.Push.Lemmas
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recall

Mathlib/Tactic/Push.lean

@@ -1,2 +1,2 @@
+import Mathlib.Tactic.Push.Attr
 import Mathlib.Tactic.Push.Basic
-import Mathlib.Tactic.Push.Lemmas

Mathlib/Tactic/Push/Attr.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Jovan Gerbscheid. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jovan Gerbscheid, Patrick Massot, Simon Hudon, Alice Laroche, Frédéric Dupuis,
+Jireh Loreaux
+-/
+import Mathlib.Init
+
+/-!
+# The `@[push]` attribute for the `push` and `push_neg` tactics
+
+This file defines the `@[push]` attribute, so that it can be used without importing
+the tactic itself.
+-/
+
+namespace Mathlib.Tactic.Push
+
+open Lean Meta
+
+/-- The `push` simp attribute. -/
+initialize pushExt : SimpExtension ← mkSimpExt
+
+/--
+The `push` attribute is used to tag lemmas that "push" a constant into an expression.
+
+For example:
+```lean
+@[push] theorem not_not (p : Prop) : ¬¬p ↔ p
+
+@[push] theorem not_imp (p q : Prop) : ¬(p → q) ↔ p ∧ ¬q
+
+@[push] theorem not_iff (p q : Prop) : ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (¬p ∧ q)
+```
+-/
+syntax (name := pushAttr) "push" ("← " <|> "<- ")? (ppSpace prio)? : attr
+
+initialize registerBuiltinAttribute {
+  name := `pushAttr
+  descr := "attribute for push"
+  add := fun decl stx kind => MetaM.run' do
+    let inv := !stx[1].isNone
+    let prio ← getAttrParamOptPrio stx[2]
+    addSimpTheorem pushExt decl (post := false) (inv := inv) kind prio
+}
+
+end Mathlib.Tactic.Push

Mathlib/Tactic/Push/Basic.lean

@@ -5,6 +5,7 @@ Authors: Jovan Gerbscheid, Patrick Massot, Simon Hudon, Alice Laroche, Frédéri
 Jireh Loreaux
 -/
 import Lean.Elab.Tactic.Location
+import Mathlib.Tactic.Push.Attr
 import Mathlib.Logic.Basic
 import Mathlib.Tactic.Conv
 
@@ -19,37 +20,14 @@ namespace Mathlib.Tactic.Push
 
 open Lean Meta Elab.Tactic Parser.Tactic
 
-section Attr
-
-/-- The `push` simp attribute. -/
-initialize pushExt : SimpExtension ← mkSimpExt
-
-/--
-The `push` attribute is used to tag lemmas that "push" a constant into an expression.
-
-For example:
-```lean
-
-```
-
-should be given to lemmas that "push" a constant towards the leaf nodes of
-an expression. The main use case is for pushing negations.
--/
-syntax (name := pushAttr) "push" ("← " <|> "<- ")? (ppSpace prio)? : attr
-
-initialize registerBuiltinAttribute {
-  name := `pushAttr
-  descr := "attribute for push"
-  add := fun decl stx kind => MetaM.run' do
-    let inv := !stx[1].isNone
-    let prio ← getAttrParamOptPrio stx[2]
-    addSimpTheorem pushExt decl (post := false) (inv := inv) kind prio
-}
+universe u v
+variable (p q : Prop) {α : Sort u} (s : α → Prop)
 
-end Attr
+-- Note: the lemma `Classical.not_imp` is attempted before `not_forall_eq`
+attribute [push] not_not not_or Classical.not_imp
 
-universe u v
-variable (p q : Prop) {α : Sort u} {β : Type v} (s : α → Prop)
+@[push] theorem not_iff : ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (¬p ∧ q) :=
+  _root_.not_iff.trans <| iff_iff_and_or_not_and_not.trans <| by rw [not_not, or_comm]
 
 theorem not_and_eq : (¬ (p ∧ q)) = (p → ¬ q) := propext not_and
 theorem not_and_or_eq : (¬ (p ∧ q)) = (¬ p ∨ ¬ q) := propext not_and_or