From 464e121719f5e1b3454ee3e05d19b38e1b771e40 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Wed, 19 Feb 2025 22:53:04 +0000 Subject: [PATCH 1/3] chore: rename PushNeg.lean to Push.lean --- Mathlib.lean | 2 +- Mathlib/Data/Nat/Basic.lean | 3 +-- Mathlib/Order/BoundedOrder/Basic.lean | 2 +- Mathlib/Tactic.lean | 2 +- Mathlib/Tactic/ByContra.lean | 2 +- Mathlib/Tactic/Common.lean | 2 +- Mathlib/Tactic/Contrapose.lean | 2 +- Mathlib/Tactic/{PushNeg.lean => Push.lean} | 0 MathlibTest/push_neg.lean | 2 +- 9 files changed, 8 insertions(+), 9 deletions(-) rename Mathlib/Tactic/{PushNeg.lean => Push.lean} (100%) diff --git a/Mathlib.lean b/Mathlib.lean index 46eb0fdeeea89..270f524b2c0fb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5286,7 +5286,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 diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 56e622d7116e1..8876640a41946 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -6,9 +6,8 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro import Mathlib.Data.Nat.Init 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.Tactic.Push import Mathlib.Util.AssertExists /-! diff --git a/Mathlib/Order/BoundedOrder/Basic.lean b/Mathlib/Order/BoundedOrder/Basic.lean index 2ad6d7f4daaf3..6c663eda464b1 100644 --- a/Mathlib/Order/BoundedOrder/Basic.lean +++ b/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 diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index c97fc4fad7b6b..ce35acffc59d6 100644 --- a/Mathlib/Tactic.lean +++ b/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 diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean index fa2859c54f3c9..878ab36a35b70 100644 --- a/Mathlib/Tactic/ByContra.lean +++ b/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 diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index e4186b76aa38f..4eb640948ba3e 100644 --- a/Mathlib/Tactic/Common.lean +++ b/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 diff --git a/Mathlib/Tactic/Contrapose.lean b/Mathlib/Tactic/Contrapose.lean index 75e5de8156361..e52a9915dfc1a 100644 --- a/Mathlib/Tactic/Contrapose.lean +++ b/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 diff --git a/Mathlib/Tactic/PushNeg.lean b/Mathlib/Tactic/Push.lean similarity index 100% rename from Mathlib/Tactic/PushNeg.lean rename to Mathlib/Tactic/Push.lean diff --git a/MathlibTest/push_neg.lean b/MathlibTest/push_neg.lean index ccfb7e34cc4a6..60fc263e068bc 100644 --- a/MathlibTest/push_neg.lean +++ b/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 From 209ea126e01521365cd33f4691843e31cc05ed64 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Wed, 19 Feb 2025 22:58:56 +0000 Subject: [PATCH 2/3] . --- Mathlib/Data/Nat/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 8876640a41946..47a38584ffce1 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -6,8 +6,8 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro import Mathlib.Data.Nat.Init import Mathlib.Logic.Function.Basic import Mathlib.Logic.Nontrivial.Defs +import Mathlib.Tactic.Contrapose import Mathlib.Tactic.GCongr.CoreAttrs -import Mathlib.Tactic.Push import Mathlib.Util.AssertExists /-! From 9d40b1f6a84337b1901197d8a3156e02613d9428 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Thu, 20 Feb 2025 01:11:09 +0000 Subject: [PATCH 3/3] update noshake --- scripts/noshake.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/noshake.json b/scripts/noshake.json index 04fb1b7b6e87b..32d438cffd9a7 100644 --- a/scripts/noshake.json +++ b/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",