refactor: remove import-only aggregator files

Delete Lean modules that only re-export their submodules via
`public import` (Foundation/FirstOrder/Basic.lean,
Foundation/FirstOrder/Completeness.lean,
Foundation/FirstOrder/Bootstrapping/Syntax.lean,
Foundation/FirstOrder/SetTheory/Basic.lean,
Foundation/FirstOrder/Arithmetic/{HFS,Definability,Exponential,Basic}.lean)
and inline their import lists into the files that imported them.
Foundation.lean is regenerated via `lake exe mk_all --module`.

Author: SnO2WMaN

Foundation.lean

@@ -1,22 +1,18 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
-public import Foundation.FirstOrder.Arithmetic.Basic
 public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy
 public import Foundation.FirstOrder.Arithmetic.Basic.Misc
 public import Foundation.FirstOrder.Arithmetic.Basic.Model
 public import Foundation.FirstOrder.Arithmetic.Basic.Monotone
-public import Foundation.FirstOrder.Arithmetic.Definability
 public import Foundation.FirstOrder.Arithmetic.Definability.Absoluteness
 public import Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable
 public import Foundation.FirstOrder.Arithmetic.Definability.Definable
 public import Foundation.FirstOrder.Arithmetic.Definability.Hierarchy
-public import Foundation.FirstOrder.Arithmetic.Exponential
 public import Foundation.FirstOrder.Arithmetic.Exponential.Bit
 public import Foundation.FirstOrder.Arithmetic.Exponential.Exp
 public import Foundation.FirstOrder.Arithmetic.Exponential.Log
 public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2
 public import Foundation.FirstOrder.Arithmetic.Exponential.Pow2
-public import Foundation.FirstOrder.Arithmetic.HFS
 public import Foundation.FirstOrder.Arithmetic.HFS.Basic
 public import Foundation.FirstOrder.Arithmetic.HFS.Coding
 public import Foundation.FirstOrder.Arithmetic.HFS.Fixpoint
@@ -36,7 +32,6 @@ public import Foundation.FirstOrder.Arithmetic.R0.Representation
 public import Foundation.FirstOrder.Arithmetic.Schemata
 public import Foundation.FirstOrder.Arithmetic.TA.Basic
 public import Foundation.FirstOrder.Arithmetic.TA.Nonstandard
-public import Foundation.FirstOrder.Basic
 public import Foundation.FirstOrder.Basic.AesopInit
 public import Foundation.FirstOrder.Basic.BinderNotation
 public import Foundation.FirstOrder.Basic.Calculus
@@ -59,7 +54,6 @@ public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D3
 public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.EquationalTheory
 public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.PeanoMinus
 public import Foundation.FirstOrder.Bootstrapping.FixedPoint
-public import Foundation.FirstOrder.Bootstrapping.Syntax
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Basic
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Coding
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Functions
@@ -74,7 +68,6 @@ public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Coding
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed
 public import Foundation.FirstOrder.Bootstrapping.Syntax.Theory
-public import Foundation.FirstOrder.Completeness
 public import Foundation.FirstOrder.Completeness.CanonicalModel
 public import Foundation.FirstOrder.Completeness.CountableSublanguage
 public import Foundation.FirstOrder.Completeness.CounterModel
@@ -108,7 +101,6 @@ public import Foundation.FirstOrder.Kripke.WeakForcing
 public import Foundation.FirstOrder.NegationTranslation.GoedelGentzen
 public import Foundation.FirstOrder.Order.Le
 public import Foundation.FirstOrder.Polarity
-public import Foundation.FirstOrder.SetTheory.Basic
 public import Foundation.FirstOrder.SetTheory.Basic.Axioms
 public import Foundation.FirstOrder.SetTheory.Basic.Misc
 public import Foundation.FirstOrder.SetTheory.Basic.Model

Foundation/FirstOrder/Arithmetic/Basic.lean

@@ -1,6 +1,10 @@
 module
 
-public import Foundation.FirstOrder.Arithmetic.Exponential
+public import Foundation.FirstOrder.Arithmetic.Exponential.Pow2
+public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2
+public import Foundation.FirstOrder.Arithmetic.Exponential.Exp
+public import Foundation.FirstOrder.Arithmetic.Exponential.Log
+public import Foundation.FirstOrder.Arithmetic.Exponential.Bit
 
 @[expose] public section
 /-!

Foundation/FirstOrder/Arithmetic/Definability.lean

@@ -1,6 +1,11 @@
 module
 
-public import Foundation.FirstOrder.Arithmetic.HFS
+public import Foundation.FirstOrder.Arithmetic.HFS.Basic
+public import Foundation.FirstOrder.Arithmetic.HFS.Seq
+public import Foundation.FirstOrder.Arithmetic.HFS.PRF
+public import Foundation.FirstOrder.Arithmetic.HFS.Fixpoint
+public import Foundation.FirstOrder.Arithmetic.HFS.Vec
+public import Foundation.FirstOrder.Arithmetic.HFS.Coding
 
 @[expose] public section
 /-!

Foundation/FirstOrder/Arithmetic/Exponential.lean

@@ -1,6 +1,10 @@
 module
 
-public import Foundation.FirstOrder.Arithmetic.Exponential
+public import Foundation.FirstOrder.Arithmetic.Exponential.Pow2
+public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2
+public import Foundation.FirstOrder.Arithmetic.Exponential.Exp
+public import Foundation.FirstOrder.Arithmetic.Exponential.Log
+public import Foundation.FirstOrder.Arithmetic.Exponential.Bit
 
 @[expose] public section
 /-!

Foundation/FirstOrder/Arithmetic/HFS.lean

@@ -1,6 +1,9 @@
 module
 
-public import Foundation.FirstOrder.Arithmetic.Definability
+public import Foundation.FirstOrder.Arithmetic.Definability.Hierarchy
+public import Foundation.FirstOrder.Arithmetic.Definability.Definable
+public import Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable
+public import Foundation.FirstOrder.Arithmetic.Definability.Absoluteness
 public import Mathlib.Algebra.Prime.Lemmas
 public import Foundation.Vorspiel.ExistsUnique
 

Foundation/FirstOrder/Arithmetic/HFS/Basic.lean

@@ -1,6 +1,9 @@
 module
 
-public import Foundation.FirstOrder.Arithmetic.Basic
+public import Foundation.FirstOrder.Arithmetic.Basic.Misc
+public import Foundation.FirstOrder.Arithmetic.Basic.Monotone
+public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy
+public import Foundation.FirstOrder.Arithmetic.Basic.Model
 
 @[expose] public section
 /-!