chore: create a Basic top folder

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
 
 /-!

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

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
 
 /-!
 

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

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

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
 
 /-!

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

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
 
 /-!

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
 

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
 
 /-!

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

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
 
 /-!
 

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
 
 /-!

Mathlib/Logic/IsEmpty.lean → 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")

Mathlib/Logic/IsEmpty/Basic.lean → 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
 
 /-!

Mathlib/Logic/Lemmas.lean → 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

Mathlib/Logic/Nontrivial/Basic.lean → 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

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.

Mathlib/Logic/Unique.lean → 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
 
 /-!

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
 
 /-!

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

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
 

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`.

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
 
 /-!

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

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
 
 /-!

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

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

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
 

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
 

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
 
 /-!

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

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
 
 /-!

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`.