diff --git a/Counterexamples/Girard.lean b/Counterexamples/Girard.lean index 16ea6890ecf9a7..41208097f6d665 100644 --- a/Counterexamples/Girard.lean +++ b/Counterexamples/Girard.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Mathlib.Logic.Basic +import Mathlib.Basic.Logic.Basic import Mathlib.Data.Set.Defs /-! diff --git a/Mathlib.lean b/Mathlib.lean index c1d24ccd4a4ae3..6c3479e42bae3d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2433,6 +2433,18 @@ public import Mathlib.Analysis.SumIntegralComparisons public import Mathlib.Analysis.SumIntegralExpDecay public import Mathlib.Analysis.SumOverResidueClass public import Mathlib.Analysis.VonNeumannAlgebra.Basic +public import Mathlib.Basic.Denumerable +public import Mathlib.Basic.ExistsUnique +public import Mathlib.Basic.IsEmpty +public import Mathlib.Basic.IsEmpty.Basic +public import Mathlib.Basic.IsEmpty.Defs +public import Mathlib.Basic.Logic.Basic +public import Mathlib.Basic.Logic.Lemmas +public import Mathlib.Basic.Nonempty +public import Mathlib.Basic.Nontrivial.Basic +public import Mathlib.Basic.Nontrivial.Defs +public import Mathlib.Basic.Unique +public import Mathlib.Basic.UnivLE public import Mathlib.CategoryTheory.Abelian.Basic public import Mathlib.CategoryTheory.Abelian.CommSq public import Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four @@ -5300,8 +5312,6 @@ public import Mathlib.LinearAlgebra.Transvection.Basic public import Mathlib.LinearAlgebra.Transvection.Generation public import Mathlib.LinearAlgebra.UnitaryGroup public import Mathlib.LinearAlgebra.Vandermonde -public import Mathlib.Logic.Basic -public import Mathlib.Logic.Denumerable public import Mathlib.Logic.Embedding.Basic public import Mathlib.Logic.Embedding.Set public import Mathlib.Logic.Encodable.Basic @@ -5326,7 +5336,6 @@ public import Mathlib.Logic.Equiv.PartialEquiv public import Mathlib.Logic.Equiv.Prod public import Mathlib.Logic.Equiv.Set public import Mathlib.Logic.Equiv.Sum -public import Mathlib.Logic.ExistsUnique public import Mathlib.Logic.Function.Basic public import Mathlib.Logic.Function.Coequalizer public import Mathlib.Logic.Function.CompTypeclasses @@ -5340,13 +5349,6 @@ public import Mathlib.Logic.Function.OfArity public import Mathlib.Logic.Function.ULift public import Mathlib.Logic.Godel.GodelBetaFunction public import Mathlib.Logic.Hydra -public import Mathlib.Logic.IsEmpty -public import Mathlib.Logic.IsEmpty.Basic -public import Mathlib.Logic.IsEmpty.Defs -public import Mathlib.Logic.Lemmas -public import Mathlib.Logic.Nonempty -public import Mathlib.Logic.Nontrivial.Basic -public import Mathlib.Logic.Nontrivial.Defs public import Mathlib.Logic.OpClass public import Mathlib.Logic.Pairwise public import Mathlib.Logic.Relation @@ -5355,8 +5357,6 @@ public import Mathlib.Logic.Small.Basic public import Mathlib.Logic.Small.Defs public import Mathlib.Logic.Small.List public import Mathlib.Logic.Small.Set -public import Mathlib.Logic.Unique -public import Mathlib.Logic.UnivLE public import Mathlib.MeasureTheory.Category.MeasCat public import Mathlib.MeasureTheory.Constructions.AddChar public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean index 13ab36b10a6970..53b503a6516628 100644 --- a/Mathlib/Algebra/CharZero/Defs.lean +++ b/Mathlib/Algebra/CharZero/Defs.lean @@ -5,8 +5,8 @@ Authors: Mario Carneiro -/ module +public import Mathlib.Basic.Logic.Basic public import Mathlib.Data.Int.Cast.Defs -public import Mathlib.Logic.Basic /-! diff --git a/Mathlib/Algebra/Group/Irreducible/Defs.lean b/Mathlib/Algebra/Group/Irreducible/Defs.lean index 000241400ae3f3..2015831f120c35 100644 --- a/Mathlib/Algebra/Group/Irreducible/Defs.lean +++ b/Mathlib/Algebra/Group/Irreducible/Defs.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Jens Wagemaker, Yaël Dillies module public import Mathlib.Algebra.Group.Units.Defs -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Logic.Basic /-! # Irreducible elements in a monoid diff --git a/Mathlib/Algebra/Group/Nat/Units.lean b/Mathlib/Algebra/Group/Nat/Units.lean index 85297dcecd5c0e..902f23b7d3a64d 100644 --- a/Mathlib/Algebra/Group/Nat/Units.lean +++ b/Mathlib/Algebra/Group/Nat/Units.lean @@ -7,7 +7,7 @@ module public import Mathlib.Algebra.Group.Nat.Defs public import Mathlib.Algebra.Group.Units.Defs -public import Mathlib.Logic.Unique +public import Mathlib.Basic.Unique /-! # The unit of the natural numbers diff --git a/Mathlib/Algebra/Group/Pi/Basic.lean b/Mathlib/Algebra/Group/Pi/Basic.lean index 1b4e34b84ed51f..e6245c835e7ea8 100644 --- a/Mathlib/Algebra/Group/Pi/Basic.lean +++ b/Mathlib/Algebra/Group/Pi/Basic.lean @@ -7,8 +7,8 @@ module public import Mathlib.Algebra.Group.Defs public import Mathlib.Algebra.Notation.Pi.Basic +public import Mathlib.Basic.Unique public import Mathlib.Data.Sum.Basic -public import Mathlib.Logic.Unique public import Mathlib.Tactic.Spread /-! diff --git a/Mathlib/Algebra/Group/Units/Basic.lean b/Mathlib/Algebra/Group/Units/Basic.lean index 1be6d4bfc6cae1..b770396b6929b3 100644 --- a/Mathlib/Algebra/Group/Units/Basic.lean +++ b/Mathlib/Algebra/Group/Units/Basic.lean @@ -8,7 +8,7 @@ module public import Mathlib.Algebra.Group.Basic public import Mathlib.Algebra.Group.Commute.Defs public import Mathlib.Algebra.Group.Units.Defs -public import Mathlib.Logic.Unique +public import Mathlib.Basic.Unique public import Mathlib.Tactic.Lift public import Mathlib.Tactic.Subsingleton public import Mathlib.Tactic.Attr.Core diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean index b61d5187b8f4a6..e888c0df8207fb 100644 --- a/Mathlib/Algebra/Group/WithOne/Defs.lean +++ b/Mathlib/Algebra/Group/WithOne/Defs.lean @@ -6,8 +6,8 @@ Authors: Mario Carneiro, Johan Commelin module public import Mathlib.Algebra.Group.Defs +public import Mathlib.Basic.Nontrivial.Basic public import Mathlib.Data.Option.Basic -public import Mathlib.Logic.Nontrivial.Basic public import Mathlib.Tactic.Common /-! diff --git a/Mathlib/Algebra/GroupWithZero/Basic.lean b/Mathlib/Algebra/GroupWithZero/Basic.lean index b645df61d0cab8..7fac13afed3b46 100644 --- a/Mathlib/Algebra/GroupWithZero/Basic.lean +++ b/Mathlib/Algebra/GroupWithZero/Basic.lean @@ -7,7 +7,7 @@ module public import Mathlib.Algebra.Group.Basic public import Mathlib.Algebra.GroupWithZero.NeZero -public import Mathlib.Logic.Unique +public import Mathlib.Basic.Unique public import Mathlib.Tactic.Conv public import Batteries.Tactic.SeqFocus diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean index 0845c14350e2d6..7fecb10fd71289 100644 --- a/Mathlib/Algebra/GroupWithZero/Defs.lean +++ b/Mathlib/Algebra/GroupWithZero/Defs.lean @@ -6,8 +6,8 @@ Authors: Johan Commelin module public import Mathlib.Algebra.Group.Defs -public import Mathlib.Logic.Nontrivial.Defs -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Nontrivial.Defs +public import Mathlib.Basic.Logic.Basic public import Batteries.Tactic.SeqFocus /-! diff --git a/Mathlib/Algebra/Module/Presentation/Free.lean b/Mathlib/Algebra/Module/Presentation/Free.lean index d8a36983dbb40a..e9ad0a3edf2d4d 100644 --- a/Mathlib/Algebra/Module/Presentation/Free.lean +++ b/Mathlib/Algebra/Module/Presentation/Free.lean @@ -6,9 +6,9 @@ Authors: Joël Riou module public import Mathlib.Algebra.Module.Presentation.Basic +public import Mathlib.Basic.UnivLE public import Mathlib.LinearAlgebra.Finsupp.VectorSpace public import Mathlib.LinearAlgebra.FreeModule.Basic -public import Mathlib.Logic.UnivLE /-! # Presentation of free modules diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean index c6bd0bb04be016..81104debfe8a80 100644 --- a/Mathlib/Algebra/Module/Projective.lean +++ b/Mathlib/Algebra/Module/Projective.lean @@ -6,8 +6,8 @@ Authors: Kevin Buzzard, Antoine Labelle module public import Mathlib.Algebra.Module.Shrink +public import Mathlib.Basic.UnivLE public import Mathlib.LinearAlgebra.TensorProduct.Basis -public import Mathlib.Logic.UnivLE /-! diff --git a/Mathlib/Algebra/NeZero.lean b/Mathlib/Algebra/NeZero.lean index de8620b16b0c76..6810e138704e85 100644 --- a/Mathlib/Algebra/NeZero.lean +++ b/Mathlib/Algebra/NeZero.lean @@ -5,7 +5,7 @@ Authors: Eric Rodriguez -/ module -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Logic.Basic public import Mathlib.Order.Defs.PartialOrder /-! diff --git a/Mathlib/Logic/Denumerable.lean b/Mathlib/Basic/Denumerable.lean similarity index 100% rename from Mathlib/Logic/Denumerable.lean rename to Mathlib/Basic/Denumerable.lean diff --git a/Mathlib/Logic/ExistsUnique.lean b/Mathlib/Basic/ExistsUnique.lean similarity index 100% rename from Mathlib/Logic/ExistsUnique.lean rename to Mathlib/Basic/ExistsUnique.lean diff --git a/Mathlib/Logic/IsEmpty.lean b/Mathlib/Basic/IsEmpty.lean similarity index 80% rename from Mathlib/Logic/IsEmpty.lean rename to Mathlib/Basic/IsEmpty.lean index c7aed45e6d6a04..42b02b11778ec3 100644 --- a/Mathlib/Logic/IsEmpty.lean +++ b/Mathlib/Basic/IsEmpty.lean @@ -8,4 +8,4 @@ module public import Mathlib.Logic.Function.Basic public import Mathlib.Logic.Relator -deprecated_module "import Mathlib.Logic.IsEmpty.Basic instead" (since := "2026-02-11") +deprecated_module "import Mathlib.Basic.IsEmpty.Basic instead" (since := "2026-02-11") diff --git a/Mathlib/Logic/IsEmpty/Basic.lean b/Mathlib/Basic/IsEmpty/Basic.lean similarity index 99% rename from Mathlib/Logic/IsEmpty/Basic.lean rename to Mathlib/Basic/IsEmpty/Basic.lean index cbc8ac01ed972c..802bce3b45978a 100644 --- a/Mathlib/Logic/IsEmpty/Basic.lean +++ b/Mathlib/Basic/IsEmpty/Basic.lean @@ -5,8 +5,8 @@ Authors: Floris van Doorn -/ module +public import Mathlib.Basic.IsEmpty.Defs public import Mathlib.Logic.Function.Basic -public import Mathlib.Logic.IsEmpty.Defs public import Mathlib.Logic.Relator /-! diff --git a/Mathlib/Logic/IsEmpty/Defs.lean b/Mathlib/Basic/IsEmpty/Defs.lean similarity index 100% rename from Mathlib/Logic/IsEmpty/Defs.lean rename to Mathlib/Basic/IsEmpty/Defs.lean diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Basic/Logic/Basic.lean similarity index 100% rename from Mathlib/Logic/Basic.lean rename to Mathlib/Basic/Logic/Basic.lean diff --git a/Mathlib/Logic/Lemmas.lean b/Mathlib/Basic/Logic/Lemmas.lean similarity index 98% rename from Mathlib/Logic/Lemmas.lean rename to Mathlib/Basic/Logic/Lemmas.lean index 0957d6c7208bcd..7ce7de942b42b8 100644 --- a/Mathlib/Logic/Lemmas.lean +++ b/Mathlib/Basic/Logic/Lemmas.lean @@ -5,7 +5,7 @@ Authors: Yaël Dillies -/ module -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Logic.Basic public import Mathlib.Tactic.Convert public import Mathlib.Tactic.SplitIfs public import Mathlib.Tactic.Tauto diff --git a/Mathlib/Logic/Nonempty.lean b/Mathlib/Basic/Nonempty.lean similarity index 100% rename from Mathlib/Logic/Nonempty.lean rename to Mathlib/Basic/Nonempty.lean diff --git a/Mathlib/Logic/Nontrivial/Basic.lean b/Mathlib/Basic/Nontrivial/Basic.lean similarity index 97% rename from Mathlib/Logic/Nontrivial/Basic.lean rename to Mathlib/Basic/Nontrivial/Basic.lean index d0eec00ab8e63f..2767cdf271c443 100644 --- a/Mathlib/Logic/Nontrivial/Basic.lean +++ b/Mathlib/Basic/Nontrivial/Basic.lean @@ -5,10 +5,10 @@ Authors: Sébastien Gouëzel -/ module +public import Mathlib.Basic.Nontrivial.Defs +public import Mathlib.Basic.Unique public import Mathlib.Data.Prod.Basic public import Mathlib.Logic.Function.Basic -public import Mathlib.Logic.Nontrivial.Defs -public import Mathlib.Logic.Unique public import Mathlib.Order.Defs.LinearOrder import Mathlib.Tactic.Attr.Register diff --git a/Mathlib/Logic/Nontrivial/Defs.lean b/Mathlib/Basic/Nontrivial/Defs.lean similarity index 100% rename from Mathlib/Logic/Nontrivial/Defs.lean rename to Mathlib/Basic/Nontrivial/Defs.lean diff --git a/Mathlib/Basic/README.md b/Mathlib/Basic/README.md new file mode 100644 index 00000000000000..8a433359a1dd15 --- /dev/null +++ b/Mathlib/Basic/README.md @@ -0,0 +1,11 @@ +# Basic mathematical properties and objects + +This folder is intended to host definitions that are used throughout mathematics without necessarily +belonging to a specific area, such as the notion of a non-empty type or the complex numbers. + +Note that results about the reals/complex numbers do not necessarily belong here. +For example, the normed group structure on them belongs in `Analysis` instead. +The order on the real numbers however belongs here because it is used to define the nonnegative real +numbers. + +The imports are meant to stay comparatively minimal. diff --git a/Mathlib/Logic/Unique.lean b/Mathlib/Basic/Unique.lean similarity index 99% rename from Mathlib/Logic/Unique.lean rename to Mathlib/Basic/Unique.lean index dae1020bde6485..8b0bb0a7de601f 100644 --- a/Mathlib/Logic/Unique.lean +++ b/Mathlib/Basic/Unique.lean @@ -5,8 +5,8 @@ Authors: Johan Commelin -/ module +public import Mathlib.Basic.IsEmpty.Defs public import Mathlib.Logic.Function.Basic -public import Mathlib.Logic.IsEmpty.Defs public import Mathlib.Tactic.Inhabit /-! diff --git a/Mathlib/Logic/UnivLE.lean b/Mathlib/Basic/UnivLE.lean similarity index 100% rename from Mathlib/Logic/UnivLE.lean rename to Mathlib/Basic/UnivLE.lean diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean index 6dd48924118145..284ee151bcc0b8 100644 --- a/Mathlib/CategoryTheory/EssentiallySmall.lean +++ b/Mathlib/CategoryTheory/EssentiallySmall.lean @@ -5,9 +5,9 @@ Authors: Kim Morrison -/ module +public import Mathlib.Basic.UnivLE public import Mathlib.CategoryTheory.Category.ULift public import Mathlib.CategoryTheory.Skeletal -public import Mathlib.Logic.UnivLE public import Mathlib.Logic.Small.Basic /-! diff --git a/Mathlib/CategoryTheory/Limits/Types/Colimits.lean b/Mathlib/CategoryTheory/Limits/Types/Colimits.lean index bd32d232cc6df7..46fb445ebdbc41 100644 --- a/Mathlib/CategoryTheory/Limits/Types/Colimits.lean +++ b/Mathlib/CategoryTheory/Limits/Types/Colimits.lean @@ -5,7 +5,7 @@ Authors: Kim Morrison, Reid Barton, Joël Riou -/ module -public import Mathlib.Logic.UnivLE +public import Mathlib.Basic.UnivLE public import Mathlib.CategoryTheory.Limits.HasLimits public import Mathlib.CategoryTheory.Limits.Types.ColimitType public import Mathlib.CategoryTheory.ConcreteCategory.Elementwise diff --git a/Mathlib/CategoryTheory/Limits/Types/Limits.lean b/Mathlib/CategoryTheory/Limits/Types/Limits.lean index e1fa0e1bf43cd9..48a2cfbd25ae38 100644 --- a/Mathlib/CategoryTheory/Limits/Types/Limits.lean +++ b/Mathlib/CategoryTheory/Limits/Types/Limits.lean @@ -5,7 +5,7 @@ Authors: Kim Morrison, Reid Barton -/ module -public import Mathlib.Logic.UnivLE +public import Mathlib.Basic.UnivLE public import Mathlib.CategoryTheory.Limits.HasLimits public import Mathlib.CategoryTheory.ConcreteCategory.Elementwise diff --git a/Mathlib/CategoryTheory/UnivLE.lean b/Mathlib/CategoryTheory/UnivLE.lean index eda0b63a2af027..c9d3f34d1b09bb 100644 --- a/Mathlib/CategoryTheory/UnivLE.lean +++ b/Mathlib/CategoryTheory/UnivLE.lean @@ -5,9 +5,9 @@ Authors: Kim Morrison -/ module +public import Mathlib.Basic.UnivLE public import Mathlib.CategoryTheory.EssentialImage public import Mathlib.CategoryTheory.Types.Basic -public import Mathlib.Logic.UnivLE /-! # Universe inequalities and essential surjectivity of `uliftFunctor`. diff --git a/Mathlib/Combinatorics/Quiver/Path.lean b/Mathlib/Combinatorics/Quiver/Path.lean index ddd9d524ee5a65..0ed4225a83217f 100644 --- a/Mathlib/Combinatorics/Quiver/Path.lean +++ b/Mathlib/Combinatorics/Quiver/Path.lean @@ -5,8 +5,8 @@ Authors: David Wärn, Kim Morrison, Matteo Cipollina -/ module +public import Mathlib.Basic.Logic.Lemmas public import Mathlib.Combinatorics.Quiver.Prefunctor -public import Mathlib.Logic.Lemmas public import Batteries.Data.List.Basic /-! diff --git a/Mathlib/Computability/Primrec/Basic.lean b/Mathlib/Computability/Primrec/Basic.lean index 70faf1d6eb86cd..536e103f5ef4e5 100644 --- a/Mathlib/Computability/Primrec/Basic.lean +++ b/Mathlib/Computability/Primrec/Basic.lean @@ -6,8 +6,8 @@ Authors: Mario Carneiro module public import Mathlib.Algebra.Order.Ring.Nat +public import Mathlib.Basic.Denumerable public import Mathlib.Logic.Function.Iterate -public import Mathlib.Logic.Denumerable /-! # The primitive recursive functions diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean index e5bb35b52875d1..379f3330aa8e7d 100644 --- a/Mathlib/Data/Bool/Basic.lean +++ b/Mathlib/Data/Bool/Basic.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad -/ module -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Logic.Basic public import Mathlib.Order.Defs.LinearOrder /-! diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean index d2162dd8f1a92f..5d4c75c9fc270e 100644 --- a/Mathlib/Data/FunLike/Basic.lean +++ b/Mathlib/Data/FunLike/Basic.lean @@ -6,8 +6,9 @@ Authors: Anne Baanen module public meta import Lean.Meta.CoeAttr + +public import Mathlib.Basic.Unique public import Mathlib.Logic.Function.Basic -public import Mathlib.Logic.Unique public import Mathlib.Util.CompileInductive public import Mathlib.Tactic.Simps.NotationClass public import Mathlib.Tactic.SplitIfs diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 3e8b01e90c6e3b..bf7b82fb6fe9b6 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -5,10 +5,10 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M -/ module +public import Mathlib.Basic.Unique public import Mathlib.Data.List.Defs public import Mathlib.Data.List.Monad public import Mathlib.Logic.OpClass -public import Mathlib.Logic.Unique public import Mathlib.Tactic.Common public import Batteries.Data.List.Lemmas public import Batteries.Tactic.Lint.Simp diff --git a/Mathlib/Data/List/GetD.lean b/Mathlib/Data/List/GetD.lean index 296b75d1659c7e..5f3b20e6732d79 100644 --- a/Mathlib/Data/List/GetD.lean +++ b/Mathlib/Data/List/GetD.lean @@ -6,8 +6,8 @@ Mario Carneiro -/ module +public import Mathlib.Basic.Logic.Basic public import Mathlib.Data.List.Defs -public import Mathlib.Logic.Basic /-! # getD and getI diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index f3999b1119c627..61c2f2011bde2f 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -5,9 +5,9 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ module +public import Mathlib.Basic.Logic.Basic +public import Mathlib.Basic.Nontrivial.Defs public import Mathlib.Data.Nat.Init -public import Mathlib.Logic.Basic -public import Mathlib.Logic.Nontrivial.Defs public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Tactic.GCongr.Core diff --git a/Mathlib/Data/Nat/MaxPowDiv.lean b/Mathlib/Data/Nat/MaxPowDiv.lean index caa09ce3da8c43..9bae1582177dcc 100644 --- a/Mathlib/Data/Nat/MaxPowDiv.lean +++ b/Mathlib/Data/Nat/MaxPowDiv.lean @@ -5,7 +5,8 @@ Authors: Matthew Robert Ballard, Yury Kudryashov -/ module -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Logic.Basic + import Mathlib.Data.Nat.Notation /-! diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean index e66b8f9b8b3ef2..678e990a9d54f1 100644 --- a/Mathlib/Data/Option/Basic.lean +++ b/Mathlib/Data/Option/Basic.lean @@ -5,9 +5,9 @@ Authors: Mario Carneiro -/ module +public import Mathlib.Basic.IsEmpty.Basic public import Mathlib.Control.Combinators public import Mathlib.Data.Option.Defs -public import Mathlib.Logic.IsEmpty.Basic public import Mathlib.Logic.Relator public import Mathlib.Util.CompileInductive public import Aesop diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean index 6b58acd862e270..f1a7041eb6f2b6 100644 --- a/Mathlib/Data/Quot.lean +++ b/Mathlib/Data/Quot.lean @@ -5,8 +5,8 @@ Authors: Johannes Hölzl -/ module +public import Mathlib.Basic.Unique public import Mathlib.Logic.Relation -public import Mathlib.Logic.Unique public import Mathlib.Util.Notation3 /-! diff --git a/Mathlib/Data/README.md b/Mathlib/Data/README.md new file mode 100644 index 00000000000000..087496b49ee5fd --- /dev/null +++ b/Mathlib/Data/README.md @@ -0,0 +1,10 @@ +# Data structures + +This folder contains results about data structures such as `List`, `Bool` or `Option`. +In an ideal world, this folder wouldn't exist as its content could reasonably be upstreamed +to either Core or Batteries. + +## TODO + +Currently this folder contains a lot of non-data structures that should move to either `Basic`, +`Algebra` or `Order`. diff --git a/Mathlib/Data/Rat/Denumerable.lean b/Mathlib/Data/Rat/Denumerable.lean index 96f3f6e8ba5826..e236d023cef421 100644 --- a/Mathlib/Data/Rat/Denumerable.lean +++ b/Mathlib/Data/Rat/Denumerable.lean @@ -5,10 +5,10 @@ Authors: Chris Hughes -/ module +public import Mathlib.Algebra.CharZero.Infinite public import Mathlib.Algebra.Ring.Rat +public import Mathlib.Basic.Denumerable public import Mathlib.Data.Rat.Encodable -public import Mathlib.Algebra.CharZero.Infinite -public import Mathlib.Logic.Denumerable /-! # Denumerability of ℚ diff --git a/Mathlib/Data/TwoPointing.lean b/Mathlib/Data/TwoPointing.lean index 53a3240d04a9f9..41fe9e3d4e57d4 100644 --- a/Mathlib/Data/TwoPointing.lean +++ b/Mathlib/Data/TwoPointing.lean @@ -5,8 +5,8 @@ Authors: Yaël Dillies -/ module -public import Mathlib.Logic.Nontrivial.Defs -public import Mathlib.Logic.Nonempty +public import Mathlib.Basic.Nonempty +public import Mathlib.Basic.Nontrivial.Defs public import Mathlib.Tactic.Simps.Basic public import Batteries.Logic diff --git a/Mathlib/Lean/Meta/CongrTheorems.lean b/Mathlib/Lean/Meta/CongrTheorems.lean index 41b8947c10bf0a..fb211caa05be85 100644 --- a/Mathlib/Lean/Meta/CongrTheorems.lean +++ b/Mathlib/Lean/Meta/CongrTheorems.lean @@ -5,9 +5,10 @@ Authors: Kyle Miller -/ module -public import Lean.Meta.Tactic.Cleanup public meta import Lean.Meta.Tactic.Refl -public import Mathlib.Logic.IsEmpty.Defs + +public import Lean.Meta.Tactic.Cleanup +public import Mathlib.Basic.IsEmpty.Defs /-! # Additions to `Lean.Meta.CongrTheorems` diff --git a/Mathlib/LinearAlgebra/Matrix/Defs.lean b/Mathlib/LinearAlgebra/Matrix/Defs.lean index a985501cb0eaf3..08b33aefc6f7b4 100644 --- a/Mathlib/LinearAlgebra/Matrix/Defs.lean +++ b/Mathlib/LinearAlgebra/Matrix/Defs.lean @@ -6,8 +6,8 @@ Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin, Lu module public import Mathlib.Algebra.Module.Pi +public import Mathlib.Basic.Nontrivial.Basic public import Mathlib.Data.Fin.Basic -public import Mathlib.Logic.Nontrivial.Basic public import Mathlib.Tactic.CrossRefAttribute /-! diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean index 54fb7aee272d45..b014d422d48a20 100644 --- a/Mathlib/Logic/Equiv/Defs.lean +++ b/Mathlib/Logic/Equiv/Defs.lean @@ -5,10 +5,10 @@ Authors: Leonardo de Moura, Mario Carneiro -/ module +public import Mathlib.Basic.Unique public import Mathlib.Data.FunLike.Equiv public import Mathlib.Data.Quot public import Mathlib.Data.Subtype -public import Mathlib.Logic.Unique public import Mathlib.Tactic.Simps.Basic public import Mathlib.Tactic.Substs diff --git a/Mathlib/Logic/Equiv/List.lean b/Mathlib/Logic/Equiv/List.lean index 4c6e52c845a488..64d135d5fe25f6 100644 --- a/Mathlib/Logic/Equiv/List.lean +++ b/Mathlib/Logic/Equiv/List.lean @@ -5,7 +5,7 @@ Authors: Mario Carneiro -/ module -public import Mathlib.Logic.Denumerable +public import Mathlib.Basic.Denumerable /-! # Equivalences involving `List`-like types diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index d2d3f67f4f10da..63e9320579aa49 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/Mathlib/Logic/Function/Basic.lean @@ -5,12 +5,12 @@ Authors: Johannes Hölzl, Mario Carneiro -/ module +public import Mathlib.Basic.ExistsUnique +public import Mathlib.Basic.Logic.Basic +public import Mathlib.Basic.Nonempty +public import Mathlib.Basic.Nontrivial.Defs public import Mathlib.Data.Set.Defs -public import Mathlib.Logic.Basic public import Mathlib.Logic.Function.Defs -public import Mathlib.Logic.ExistsUnique -public import Mathlib.Logic.Nonempty -public import Mathlib.Logic.Nontrivial.Defs public import Batteries.Tactic.Init public import Mathlib.Order.Defs.Unbundled diff --git a/Mathlib/Logic/README.md b/Mathlib/Logic/README.md new file mode 100644 index 00000000000000..252b4fc5b70576 --- /dev/null +++ b/Mathlib/Logic/README.md @@ -0,0 +1,17 @@ +# Logic + +This folder contains results about advanced mathematical logic. + +Note that model theory results should instead go to the `ModelTheory` folder and set theory results +to the `SetTheory` one. + +## Content + +Currently we provide: +* The termination of the hydra game. +* Gödel's Beta function lemma + +## TODO + +Currently this folder contains a lot of basic logic results that should move to either `Basic` or +`Order`. diff --git a/Mathlib/Order/OrderIsoNat.lean b/Mathlib/Order/OrderIsoNat.lean index 51c1dcdaa3349b..8b7a391dd92f32 100644 --- a/Mathlib/Order/OrderIsoNat.lean +++ b/Mathlib/Order/OrderIsoNat.lean @@ -5,8 +5,8 @@ Authors: Mario Carneiro -/ module +public import Mathlib.Basic.Denumerable public import Mathlib.Data.Set.Subsingleton -public import Mathlib.Logic.Denumerable public import Mathlib.Logic.Function.Iterate public import Mathlib.Order.Hom.Basic public import Mathlib.Order.Lattice.Nat diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean index ffdfdd4ad82556..59e57b6de2c429 100644 --- a/Mathlib/Order/RelClasses.lean +++ b/Mathlib/Order/RelClasses.lean @@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Yury Kudryashov -/ module -public import Mathlib.Logic.IsEmpty.Basic +public import Mathlib.Basic.IsEmpty.Basic public import Mathlib.Order.OrderDual public import Mathlib.Tactic.CrossRefAttribute public import Mathlib.Tactic.MkIffOfInductiveProp diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean index 330fe865bdd45f..6faa953749f7db 100644 --- a/Mathlib/Order/WithBot.lean +++ b/Mathlib/Order/WithBot.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl -/ module -public import Mathlib.Logic.Nontrivial.Basic +public import Mathlib.Basic.Nontrivial.Basic public import Mathlib.Order.TypeTags public import Mathlib.Data.Option.NAry public import Mathlib.Tactic.Contrapose diff --git a/Mathlib/RingTheory/Coprime/Basic.lean b/Mathlib/RingTheory/Coprime/Basic.lean index 2b88d64f35a22c..3f0538c008d38b 100644 --- a/Mathlib/RingTheory/Coprime/Basic.lean +++ b/Mathlib/RingTheory/Coprime/Basic.lean @@ -10,7 +10,7 @@ public import Mathlib.Algebra.Group.Nat.Units public import Mathlib.Algebra.GroupWithZero.Associated public import Mathlib.Algebra.Ring.Divisibility.Basic public import Mathlib.Algebra.Ring.Hom.Defs -public import Mathlib.Logic.Basic +public import Mathlib.Basic.Logic.Basic public import Mathlib.Tactic.CrossRefAttribute public import Mathlib.Tactic.Ring diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 63ee719ca69174..9536659d34cfa3 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -5,13 +5,13 @@ Authors: Johannes Hölzl, Mario Carneiro, Floris van Doorn -/ module +public import Mathlib.Basic.UnivLE public import Mathlib.Data.Countable.Small public import Mathlib.Data.Fintype.BigOperators public import Mathlib.Data.Fintype.Powerset public import Mathlib.Data.Nat.Cast.Order.Basic public import Mathlib.Data.Set.Countable public import Mathlib.Logic.Small.Set -public import Mathlib.Logic.UnivLE public import Mathlib.SetTheory.Cardinal.Order /-! diff --git a/Mathlib/SetTheory/Cardinal/UnivLE.lean b/Mathlib/SetTheory/Cardinal/UnivLE.lean index fb7b478efdf25d..f0e60a4631c09c 100644 --- a/Mathlib/SetTheory/Cardinal/UnivLE.lean +++ b/Mathlib/SetTheory/Cardinal/UnivLE.lean @@ -5,7 +5,7 @@ Authors: Junyan Xu -/ module -public import Mathlib.Logic.UnivLE +public import Mathlib.Basic.UnivLE public import Mathlib.SetTheory.Ordinal.Univ /-! diff --git a/Mathlib/SetTheory/ZFC/Rank.lean b/Mathlib/SetTheory/ZFC/Rank.lean index 340976356e7341..fb0e6402c4a198 100644 --- a/Mathlib/SetTheory/ZFC/Rank.lean +++ b/Mathlib/SetTheory/ZFC/Rank.lean @@ -5,7 +5,7 @@ Authors: Dexin Zhang -/ module -public import Mathlib.Logic.UnivLE +public import Mathlib.Basic.UnivLE public import Mathlib.SetTheory.Ordinal.Rank public import Mathlib.SetTheory.ZFC.Basic diff --git a/Mathlib/Tactic/CancelDenoms/Core.lean b/Mathlib/Tactic/CancelDenoms/Core.lean index cd2312f16aa0a1..c29619c05eedb6 100644 --- a/Mathlib/Tactic/CancelDenoms/Core.lean +++ b/Mathlib/Tactic/CancelDenoms/Core.lean @@ -5,9 +5,11 @@ Authors: Robert Y. Lewis -/ module +public meta import Mathlib.Algebra.Group.Nat.Defs +public meta import Mathlib.Basic.Logic.Basic public meta import Mathlib.Data.Tree.Basic + public import Mathlib.Algebra.Field.Basic -public meta import Mathlib.Algebra.Group.Nat.Defs public import Mathlib.Algebra.Order.Ring.Defs public import Mathlib.Data.Tree.Basic public import Mathlib.Tactic.NormNum.Core diff --git a/Mathlib/Tactic/CongrExclamation.lean b/Mathlib/Tactic/CongrExclamation.lean index fdf409fcf2fed4..d4759d5fb707a7 100644 --- a/Mathlib/Tactic/CongrExclamation.lean +++ b/Mathlib/Tactic/CongrExclamation.lean @@ -9,8 +9,9 @@ public meta import Lean.Elab.ConfigEval public meta import Lean.Elab.Tactic.RCases public meta import Lean.Meta.Tactic.Assumption public meta import Lean.Meta.Tactic.Rfl +public meta import Mathlib.Basic.Logic.Basic public meta import Mathlib.Lean.Meta.CongrTheorems -public import Mathlib.Logic.Basic + public import Mathlib.Lean.Meta.CongrTheorems /-! diff --git a/Mathlib/Tactic/ITauto.lean b/Mathlib/Tactic/ITauto.lean index aea71f5ee3d8d5..042badf4019c52 100644 --- a/Mathlib/Tactic/ITauto.lean +++ b/Mathlib/Tactic/ITauto.lean @@ -5,11 +5,12 @@ Authors: Mario Carneiro -/ module -public import Mathlib.Logic.Basic -- shake: keep (Qq output dependency) public meta import Mathlib.Util.AtomM public meta import Qq + public import Batteries.Tactic.Exact public import Batteries.Tactic.Init +public import Mathlib.Basic.Logic.Basic -- shake: keep (Qq output dependency) public import Mathlib.Util.AtomM /-! diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index 9e9bd3ca160442..7b0d821c163ad2 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -204,12 +204,13 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic.Lemma), (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic.ToAdditive), (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic), -- split this up further? + (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Basic), (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Data), -- split this up further? (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Algebra.Notation), (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Data.Notation), (`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Data.Array), - (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Data), + (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Basic), (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Logic), (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Order.Defs), (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Tactic), @@ -218,6 +219,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Logic), (`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Tactic.Trans), (`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Tactic.Init), + (`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Basic), (`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Data), (`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Order), (`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Logic), @@ -236,6 +238,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Elab.InfoTree), (`Mathlib.Logic, `Batteries), + (`Mathlib.Logic, `Mathlib.Basic), -- TODO: should the next import direction be flipped? (`Mathlib.Logic, `Mathlib.Control), (`Mathlib.Logic, `Mathlib.Lean), @@ -261,13 +264,14 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Testing, `Batteries), -- TODO: this next import should be eliminated. - (`Mathlib.Testing, `Mathlib.GroupTheory), - (`Mathlib.Testing, `Mathlib.Control), (`Mathlib.Testing, `Mathlib.Algebra), + (`Mathlib.Testing, `Mathlib.Basic), + (`Mathlib.Testing, `Mathlib.Control), (`Mathlib.Testing, `Mathlib.Data), + (`Mathlib.Testing, `Mathlib.GroupTheory), + (`Mathlib.Testing, `Mathlib.Lean), (`Mathlib.Testing, `Mathlib.Logic), (`Mathlib.Testing, `Mathlib.Order), - (`Mathlib.Testing, `Mathlib.Lean), (`Mathlib.Testing, `Mathlib.Tactic), (`Mathlib.Testing, `Mathlib.Util), ] @@ -332,6 +336,20 @@ def forbiddenImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Analysis, `Mathlib.RepresentationTheory), (`Mathlib.Analysis, `Mathlib.Testing), (`Mathlib.Analysis.Calculus, `Mathlib.AlgebraicTopology), + (`Mathlib.Basic, `Mathlib.AlgebraicGeometry), + (`Mathlib.Basic, `Mathlib.AlgebraicTopology), + (`Mathlib.Basic, `Mathlib.Analysis), + (`Mathlib.Basic, `Mathlib.Computability), + (`Mathlib.Basic, `Mathlib.Condensed), + (`Mathlib.Basic, `Mathlib.FieldTheory), + (`Mathlib.Basic, `Mathlib.Geometry.Euclidean), + (`Mathlib.Basic, `Mathlib.Geometry.Group), + (`Mathlib.Basic, `Mathlib.Geometry.Manifold), + (`Mathlib.Basic, `Mathlib.Geometry.RingedSpace), + (`Mathlib.Basic, `Mathlib.InformationTheory), + (`Mathlib.Basic, `Mathlib.ModelTheory), + (`Mathlib.Basic, `Mathlib.RepresentationTheory), + (`Mathlib.Basic, `Mathlib.Testing), (`Mathlib.CategoryTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.CategoryTheory, `Mathlib.Analysis), (`Mathlib.CategoryTheory, `Mathlib.Computability), diff --git a/Mathlib/Tactic/Nontriviality/Core.lean b/Mathlib/Tactic/Nontriviality/Core.lean index 2c99f49ac864d2..76cfea28e00c05 100644 --- a/Mathlib/Tactic/Nontriviality/Core.lean +++ b/Mathlib/Tactic/Nontriviality/Core.lean @@ -5,11 +5,12 @@ Authors: Sébastien Gouëzel, Mario Carneiro -/ module -public meta import Qq.MetaM -public import Mathlib.Logic.Nontrivial.Basic -- shake: keep (tactic dependency) -public import Mathlib.Tactic.Attr.Register -- shake: keep (tactic dependency) public meta import Lean.Elab.Tactic.Meta public meta import Lean.Elab.Tactic.SolveByElim +public meta import Qq.MetaM + +public import Mathlib.Basic.Nontrivial.Basic -- shake: keep (tactic dependency) +public import Mathlib.Tactic.Attr.Register -- shake: keep (tactic dependency) /-! # The `nontriviality` tactic. -/ diff --git a/Mathlib/Tactic/Push.lean b/Mathlib/Tactic/Push.lean index 3ebc12e181ebcf..9cfa737e7c5ff4 100644 --- a/Mathlib/Tactic/Push.lean +++ b/Mathlib/Tactic/Push.lean @@ -6,9 +6,10 @@ Jireh Loreaux -/ module -public meta import Lean.Elab.Tactic.Conv.Simp public meta import Lean.Elab.ConfigEval -public import Mathlib.Logic.Basic +public meta import Lean.Elab.Tactic.Conv.Simp + +public import Mathlib.Basic.Logic.Basic public import Mathlib.Tactic.Conv public import Mathlib.Tactic.Push.Attr public import Mathlib.Util.AtLocation diff --git a/Mathlib/Tactic/Subsingleton.lean b/Mathlib/Tactic/Subsingleton.lean index 5836c129df0772..bdbef7ba4e688c 100644 --- a/Mathlib/Tactic/Subsingleton.lean +++ b/Mathlib/Tactic/Subsingleton.lean @@ -6,7 +6,8 @@ Authors: Kyle Miller module public meta import Lean.Meta.Tactic.Refl -public import Mathlib.Logic.Basic + +public import Mathlib.Basic.Logic.Basic /-! # `subsingleton` tactic diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean index dcfc8e0826ee02..a7d0030b46dc69 100644 --- a/Mathlib/Tactic/Tauto.lean +++ b/Mathlib/Tactic/Tauto.lean @@ -7,9 +7,10 @@ module public meta import Lean.Elab.Tactic.Classical public meta import Lean.Elab.Tactic.Config -public import Mathlib.Logic.Basic -- shake: keep (dependency of tactic output) -public meta import Qq public meta import Mathlib.Lean.Meta +public meta import Qq + +public import Mathlib.Basic.Logic.Basic -- shake: keep (dependency of tactic output) public import Mathlib.Tactic.CasesM public import Mathlib.Tactic.Core diff --git a/Mathlib/Testing/Plausible/Testable.lean b/Mathlib/Testing/Plausible/Testable.lean index 75b3d9de3b6a33..a07912460b6d77 100644 --- a/Mathlib/Testing/Plausible/Testable.lean +++ b/Mathlib/Testing/Plausible/Testable.lean @@ -5,11 +5,12 @@ Authors: Henrik Böving, Simon Hudon -/ module -public import Plausible.Testable -public meta import Mathlib.Logic.Basic +public meta import Mathlib.Basic.Logic.Basic +public meta import Plausible.Testable + public import Mathlib.Tactic.Basic public import Plausible.Gen -public meta import Plausible.Testable +public import Plausible.Testable /-! This module contains `Plausible.Testable` and `Plausible.PrintableProb` instances for mathlib types. diff --git a/Mathlib/Topology/Order/UpperLowerSetTopology.lean b/Mathlib/Topology/Order/UpperLowerSetTopology.lean index c6152ebd84023e..64d933828a26a8 100644 --- a/Mathlib/Topology/Order/UpperLowerSetTopology.lean +++ b/Mathlib/Topology/Order/UpperLowerSetTopology.lean @@ -5,7 +5,7 @@ Authors: Christopher Hoskin -/ module -public import Mathlib.Logic.Lemmas +public import Mathlib.Basic.Logic.Lemmas public import Mathlib.Topology.AlexandrovDiscrete public import Mathlib.Topology.ContinuousMap.Basic public import Mathlib.Topology.Order.LowerUpperTopology diff --git a/MathlibTest/Linter/PrivateModule/ImportOnly.lean b/MathlibTest/Linter/PrivateModule/ImportOnly.lean index 4dca009e17257c..db57d51633f1b0 100644 --- a/MathlibTest/Linter/PrivateModule/ImportOnly.lean +++ b/MathlibTest/Linter/PrivateModule/ImportOnly.lean @@ -1,7 +1,7 @@ module +import Mathlib.Basic.Logic.Basic import Mathlib.Tactic.Linter.PrivateModule -import Mathlib.Logic.Basic set_option linter.privateModule true diff --git a/scripts/autolabel.lean b/scripts/autolabel.lean index 20ae2508666034..dfffb6f5c38336 100644 --- a/scripts/autolabel.lean +++ b/scripts/autolabel.lean @@ -201,6 +201,7 @@ def mathlibLabelData : (l : Label) → LabelData l dependencies := #[.«t-algebra»] } | .«t-data» => { dirs := #[ + "Mathlib" / "Basic", "Mathlib" / "Control", "Mathlib" / "Data"] } | .«t-differential-geometry» => { diff --git a/scripts/noshake.json b/scripts/noshake.json index b2d50ab4febb68..eace2d02653f76 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -232,12 +232,12 @@ "Mathlib.Tactic.ToExpr": ["Mathlib.Tactic.AdaptationNote"], "Mathlib.Tactic.ToDual": ["Mathlib.Tactic.Translate.ToDual"], "Mathlib.Tactic.ToAdditive": ["Mathlib.Tactic.Translate.ToAdditive"], - "Mathlib.Tactic.TermCongr": ["Mathlib.Logic.Basic"], + "Mathlib.Tactic.TermCongr": ["Mathlib.Basic.Logic.Basic"], "Mathlib.Tactic.TautoSet": ["Mathlib.Data.Set.Disjoint", "Mathlib.Data.Set.SymmDiff"], - "Mathlib.Tactic.Tauto": ["Mathlib.Logic.Basic"], + "Mathlib.Tactic.Tauto": ["Mathlib.Basic.Logic.Basic"], "Mathlib.Tactic.TFAE": ["Mathlib.Data.List.TFAE", "Mathlib.Tactic.Have"], - "Mathlib.Tactic.Subsingleton": ["Mathlib.Logic.Basic", "Std.Logic"], + "Mathlib.Tactic.Subsingleton": ["Mathlib.Basic.Logic.Basic", "Std.Logic"], "Mathlib.Tactic.Simps.Basic": ["Batteries.Data.String.Basic"], "Mathlib.Tactic.Says": ["Batteries.Data.String.Basic"], "Mathlib.Tactic.Ring.NamePolyVars": ["Mathlib.Algebra.MvPolynomial.Basic"], @@ -266,7 +266,7 @@ "Mathlib.Tactic.NormNum.BigOperators": ["Mathlib.Algebra.BigOperators.Group.Finset.Basic", "Mathlib.Data.List.FinRange"], - "Mathlib.Tactic.Nontriviality.Core": ["Mathlib.Logic.Nontrivial.Basic"], + "Mathlib.Tactic.Nontriviality.Core": ["Mathlib.Basic.Nontrivial.Basic"], "Mathlib.Tactic.NoncommRing": ["Mathlib.Algebra.Group.Action.Defs"], "Mathlib.Tactic.MoveAdd": ["Mathlib.Algebra.Group.Basic", @@ -281,7 +281,7 @@ "Mathlib.Tactic.Lemma": ["Lean.Parser.Command"], "Mathlib.Tactic.IrreducibleDef": ["Mathlib.Data.Subtype", "Mathlib.Util.TermReduce"], - "Mathlib.Tactic.ITauto": ["Batteries.Tactic.Init", "Mathlib.Logic.Basic"], + "Mathlib.Tactic.ITauto": ["Batteries.Tactic.Init", "Mathlib.Basic.Logic.Basic"], "Mathlib.Tactic.Group": ["Mathlib.Algebra.Group.Commutator"], "Mathlib.Tactic.GCongr.CoreAttrs": ["Mathlib.Tactic.GCongr.Core"], "Mathlib.Tactic.GCongr.Core": ["Mathlib.Order.Defs"], @@ -317,7 +317,7 @@ "Mathlib.Tactic.ContinuousFunctionalCalculus": ["Mathlib.Tactic.FunProp"], "Mathlib.Tactic.Continuity": ["Mathlib.Tactic.Continuity.Init"], "Mathlib.Tactic.CongrM": ["Mathlib.Tactic.WithoutCDot"], - "Mathlib.Tactic.CongrExclamation": ["Mathlib.Logic.Basic"], + "Mathlib.Tactic.CongrExclamation": ["Mathlib.Basic.Logic.Basic"], "Mathlib.Tactic.Choose": ["Mathlib.Logic.Function.Basic"], "Mathlib.Tactic.CategoryTheory.ToApp": ["Mathlib.CategoryTheory.Category.Cat"], @@ -396,15 +396,15 @@ "Mathlib.MeasureTheory.MeasurableSpace.Embedding": ["Mathlib.Tactic.FunProp"], "Mathlib.MeasureTheory.MeasurableSpace.Defs": ["Mathlib.Tactic.FunProp.Attr"], "Mathlib.ModelTheory.Definability": ["Mathlib.Tactic.FunProp"], - "Mathlib.Logic.Relation": ["Mathlib.Logic.Basic"], - "Mathlib.Logic.Nontrivial.Defs": ["Mathlib.Init.Logic"], + "Mathlib.Logic.Relation": ["Mathlib.Basic.Logic.Basic"], + "Mathlib.Basic.Nontrivial.Defs": ["Mathlib.Init.Logic"], "Mathlib.Logic.Function.Defs": ["Mathlib.Tactic.AdaptationNote"], "Mathlib.Logic.Function.Basic": ["Batteries.Tactic.Init"], "Mathlib.Logic.Equiv.Prod": ["Mathlib.Data.Prod.PProd"], "Mathlib.Logic.Equiv.Fin.Basic": ["Batteries.Data.Fin.Lemmas"], "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic", "Mathlib.Data.Subtype"], - "Mathlib.Logic.Basic": + "Mathlib.Basic.Logic.Basic": ["Batteries.Tactic.Trans", "Mathlib.Tactic.AdaptationNote"], "Mathlib.LinearAlgebra.Matrix.Transvection": ["Mathlib.Data.Matrix.DMatrix"], "Mathlib.LinearAlgebra.DFinsupp": ["Mathlib.LinearAlgebra.Finsupp.SumProd"],