chore: rename PushNeg.lean to Push.lean (#22108)

This PR renames the file `PushNeg.lean` to `Push.lean`, to help reviewing #21965.

It also removes an import of PushNeg where it is already transitively imported

Mathlib.lean

@@ -5292,7 +5292,7 @@ import Mathlib.Tactic.ProdAssoc
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.ProxyType
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recall

Mathlib/Data/Nat/Basic.lean

@@ -8,7 +8,6 @@ import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Nontrivial.Defs
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.GCongr.CoreAttrs
-import Mathlib.Tactic.PushNeg
 import Mathlib.Util.AssertExists
 
 /-!

Mathlib/Order/BoundedOrder/Basic.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Order.Max
 import Mathlib.Order.ULift
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 import Mathlib.Tactic.Finiteness.Attr
 import Mathlib.Util.AssertExists
 

Mathlib/Tactic.lean

@@ -206,7 +206,7 @@ import Mathlib.Tactic.ProdAssoc
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.ProxyType
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recall

Mathlib/Tactic/ByContra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard
 -/
 import Batteries.Tactic.Init
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 
 /-!
 # The `by_contra` tactic

Mathlib/Tactic/Common.lean

@@ -76,7 +76,7 @@ import Mathlib.Tactic.OfNat
 -- import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recover
 import Mathlib.Tactic.Relation.Rfl

Mathlib/Tactic/Contrapose.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
 
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 
 /-! # Contrapose
 

MathlibTest/push_neg.lean

@@ -5,7 +5,7 @@ Authors: Alice Laroche, Frédéric Dupuis, Jireh Loreaux
 -/
 
 import Mathlib.Order.Defs.LinearOrder
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
 
 private axiom test_sorry : ∀ {α}, α
 set_option autoImplicit true

scripts/noshake.json

@@ -143,7 +143,7 @@
   "Mathlib.Tactic.Positivity.Basic",
   "Mathlib.Tactic.Positivity.Finset",
   "Mathlib.Tactic.ProjectionNotation",
-  "Mathlib.Tactic.PushNeg",
+  "Mathlib.Tactic.Push",
   "Mathlib.Tactic.Qify",
   "Mathlib.Tactic.RSuffices",
   "Mathlib.Tactic.Recover",