chore: create a Basic top folder

Move a select few folders from `Logic` to a new `basic` folder. The goal is to finally move the material misplaced in the `Data` and `Logic` folder.

Many more files (~1000) could be moved, so I will do it in several PRs.

This PR stems from discussions at the MI retreat 2026.

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.Basic
 import Mathlib.Data.Set.Defs
 
 /-!

Mathlib.lean

@@ -5205,8 +5205,8 @@ 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.Basic.Basic
+public import Mathlib.Basic.Denumerable
 public import Mathlib.Logic.Embedding.Basic
 public import Mathlib.Logic.Embedding.Set
 public import Mathlib.Logic.Encodable.Basic
@@ -5231,7 +5231,7 @@ 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.Basic.ExistsUnique
 public import Mathlib.Logic.Function.Basic
 public import Mathlib.Logic.Function.Coequalizer
 public import Mathlib.Logic.Function.CompTypeclasses
@@ -5245,13 +5245,13 @@ 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.Basic.IsEmpty
+public import Mathlib.Basic.IsEmpty.Basic
+public import Mathlib.Basic.IsEmpty.Defs
+public import Mathlib.Basic.Lemmas
+public import Mathlib.Basic.Nonempty
+public import Mathlib.Basic.Nontrivial.Basic
+public import Mathlib.Basic.Nontrivial.Defs
 public import Mathlib.Logic.OpClass
 public import Mathlib.Logic.Pairwise
 public import Mathlib.Logic.Relation
@@ -5260,8 +5260,8 @@ 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.Basic.Unique
+public import Mathlib.Basic.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

@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 module
 
 public import Mathlib.Data.Int.Cast.Defs
-public import Mathlib.Logic.Basic
+public import Mathlib.Basic.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.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

@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.Group.Defs
 public import Mathlib.Algebra.Notation.Pi.Basic
 public import Mathlib.Data.Sum.Basic
-public import Mathlib.Logic.Unique
+public import Mathlib.Basic.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

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Group.Defs
 public import Mathlib.Data.Option.Basic
-public import Mathlib.Logic.Nontrivial.Basic
+public import Mathlib.Basic.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.Basic
 public import Batteries.Tactic.SeqFocus
 
 /-!