chore: create a Basic top folder

Author: YaelDillies

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

@@ -2399,6 +2399,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
@@ -5214,8 +5226,6 @@ public import Mathlib.LinearAlgebra.Transvection
 public import Mathlib.LinearAlgebra.Transvection.Basic
 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
@@ -5240,7 +5250,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
@@ -5254,13 +5263,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
@@ -5269,8 +5271,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
 
 /-!