From b0a30ed4b4b979c0109577bc4f73abd0181ce258 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Mon, 8 May 2023 13:37:02 -0600
Subject: [PATCH] Rename `Bookshelf` to `Common`.

---
 Bookshelf.lean                                      | 4 ----
 Bookshelf/Combinator.lean                           | 1 -
 Bookshelf/LTuple.lean                               | 1 -
 Bookshelf/List.lean                                 | 1 -
 Bookshelf/Real.lean                                 | 7 -------
 Bookshelf/Real/Function.lean                        | 1 -
 Bookshelf/Real/Geometry.lean                        | 3 ---
 Bookshelf/Real/Sequence.lean                        | 2 --
 Bookshelf/Real/Set.lean                             | 3 ---
 Common.lean                                         | 4 ++++
 Common/Combinator.lean                              | 1 +
 {Bookshelf => Common}/Combinator/Aviary.lean        | 2 +-
 Common/LTuple.lean                                  | 1 +
 {Bookshelf => Common}/LTuple/Basic.lean             | 2 +-
 Common/List.lean                                    | 1 +
 {Bookshelf => Common}/List/Basic.lean               | 2 +-
 Common/Real.lean                                    | 7 +++++++
 {Bookshelf => Common}/Real/Basic.lean               | 2 +-
 Common/Real/Function.lean                           | 1 +
 {Bookshelf => Common}/Real/Function/Step.lean       | 6 +++---
 Common/Real/Geometry.lean                           | 3 +++
 {Bookshelf => Common}/Real/Geometry/Area.lean       | 6 +++---
 {Bookshelf => Common}/Real/Geometry/Basic.lean      | 5 +++--
 {Bookshelf => Common}/Real/Geometry/Rectangle.lean  | 4 ++--
 {Bookshelf => Common}/Real/Int.lean                 | 5 +++++
 {Bookshelf => Common}/Real/Rational.lean            | 4 ++--
 Common/Real/Sequence.lean                           | 2 ++
 {Bookshelf => Common}/Real/Sequence/Arithmetic.lean | 2 +-
 {Bookshelf => Common}/Real/Sequence/Arithmetic.tex  | 2 +-
 {Bookshelf => Common}/Real/Sequence/Geometric.lean  | 2 +-
 {Bookshelf => Common}/Real/Sequence/Geometric.tex   | 2 +-
 Common/Real/Set.lean                                | 3 +++
 {Bookshelf => Common}/Real/Set/Basic.lean           | 2 +-
 {Bookshelf => Common}/Real/Set/Interval.lean        | 2 +-
 {Bookshelf => Common}/Real/Set/Partition.lean       | 7 ++++---
 Exercises/Apostol/Chapter_1_07.tex                  | 4 ++--
 Exercises/Apostol/Chapter_1_11.lean                 | 3 ++-
 Exercises/Apostol/Chapter_I_03.lean                 | 2 +-
 Exercises/Enderton/Chapter0.lean                    | 2 +-
 lakefile.lean                                       | 2 +-
 40 files changed, 62 insertions(+), 54 deletions(-)
 delete mode 100644 Bookshelf.lean
 delete mode 100644 Bookshelf/Combinator.lean
 delete mode 100644 Bookshelf/LTuple.lean
 delete mode 100644 Bookshelf/List.lean
 delete mode 100644 Bookshelf/Real.lean
 delete mode 100644 Bookshelf/Real/Function.lean
 delete mode 100644 Bookshelf/Real/Geometry.lean
 delete mode 100644 Bookshelf/Real/Sequence.lean
 delete mode 100644 Bookshelf/Real/Set.lean
 create mode 100644 Common.lean
 create mode 100644 Common/Combinator.lean
 rename {Bookshelf => Common}/Combinator/Aviary.lean (99%)
 create mode 100644 Common/LTuple.lean
 rename {Bookshelf => Common}/LTuple/Basic.lean (99%)
 create mode 100644 Common/List.lean
 rename {Bookshelf => Common}/List/Basic.lean (99%)
 create mode 100644 Common/Real.lean
 rename {Bookshelf => Common}/Real/Basic.lean (93%)
 create mode 100644 Common/Real/Function.lean
 rename {Bookshelf => Common}/Real/Function/Step.lean (94%)
 create mode 100644 Common/Real/Geometry.lean
 rename {Bookshelf => Common}/Real/Geometry/Area.lean (97%)
 rename {Bookshelf => Common}/Real/Geometry/Basic.lean (96%)
 rename {Bookshelf => Common}/Real/Geometry/Rectangle.lean (97%)
 rename {Bookshelf => Common}/Real/Int.lean (56%)
 rename {Bookshelf => Common}/Real/Rational.lean (86%)
 create mode 100644 Common/Real/Sequence.lean
 rename {Bookshelf => Common}/Real/Sequence/Arithmetic.lean (98%)
 rename {Bookshelf => Common}/Real/Sequence/Arithmetic.tex (92%)
 rename {Bookshelf => Common}/Real/Sequence/Geometric.lean (98%)
 rename {Bookshelf => Common}/Real/Sequence/Geometric.tex (92%)
 create mode 100644 Common/Real/Set.lean
 rename {Bookshelf => Common}/Real/Set/Basic.lean (96%)
 rename {Bookshelf => Common}/Real/Set/Interval.lean (90%)
 rename {Bookshelf => Common}/Real/Set/Partition.lean (96%)

diff --git a/Bookshelf.lean b/Bookshelf.lean
deleted file mode 100644
index 62113ba..0000000
--- a/Bookshelf.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import Bookshelf.Combinator
-import Bookshelf.List
-import Bookshelf.LTuple
-import Bookshelf.Real
diff --git a/Bookshelf/Combinator.lean b/Bookshelf/Combinator.lean
deleted file mode 100644
index fc825e4..0000000
--- a/Bookshelf/Combinator.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Bookshelf.Combinator.Aviary
\ No newline at end of file
diff --git a/Bookshelf/LTuple.lean b/Bookshelf/LTuple.lean
deleted file mode 100644
index 3eadafb..0000000
--- a/Bookshelf/LTuple.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Bookshelf.LTuple.Basic
\ No newline at end of file
diff --git a/Bookshelf/List.lean b/Bookshelf/List.lean
deleted file mode 100644
index e86566b..0000000
--- a/Bookshelf/List.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Bookshelf.List.Basic
diff --git a/Bookshelf/Real.lean b/Bookshelf/Real.lean
deleted file mode 100644
index fb2bc18..0000000
--- a/Bookshelf/Real.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-import Bookshelf.Real.Basic
-import Bookshelf.Real.Function
-import Bookshelf.Real.Geometry
-import Bookshelf.Real.Int
-import Bookshelf.Real.Rational
-import Bookshelf.Real.Sequence
-import Bookshelf.Real.Set
diff --git a/Bookshelf/Real/Function.lean b/Bookshelf/Real/Function.lean
deleted file mode 100644
index f08462d..0000000
--- a/Bookshelf/Real/Function.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Bookshelf.Real.Function.Step
\ No newline at end of file
diff --git a/Bookshelf/Real/Geometry.lean b/Bookshelf/Real/Geometry.lean
deleted file mode 100644
index e890849..0000000
--- a/Bookshelf/Real/Geometry.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Bookshelf.Real.Geometry.Area
-import Bookshelf.Real.Geometry.Basic
-import Bookshelf.Real.Geometry.Rectangle
\ No newline at end of file
diff --git a/Bookshelf/Real/Sequence.lean b/Bookshelf/Real/Sequence.lean
deleted file mode 100644
index 0bfafc5..0000000
--- a/Bookshelf/Real/Sequence.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Bookshelf.Real.Sequence.Arithmetic
-import Bookshelf.Real.Sequence.Geometric
diff --git a/Bookshelf/Real/Set.lean b/Bookshelf/Real/Set.lean
deleted file mode 100644
index 9c77974..0000000
--- a/Bookshelf/Real/Set.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Bookshelf.Real.Set.Basic
-import Bookshelf.Real.Set.Interval
-import Bookshelf.Real.Set.Partition
\ No newline at end of file
diff --git a/Common.lean b/Common.lean
new file mode 100644
index 0000000..0217707
--- /dev/null
+++ b/Common.lean
@@ -0,0 +1,4 @@
+import Common.Combinator
+import Common.List
+import Common.LTuple
+import Common.Real
diff --git a/Common/Combinator.lean b/Common/Combinator.lean
new file mode 100644
index 0000000..1ff30b1
--- /dev/null
+++ b/Common/Combinator.lean
@@ -0,0 +1 @@
+import Common.Combinator.Aviary
\ No newline at end of file
diff --git a/Bookshelf/Combinator/Aviary.lean b/Common/Combinator/Aviary.lean
similarity index 99%
rename from Bookshelf/Combinator/Aviary.lean
rename to Common/Combinator/Aviary.lean
index 966ca98..203592e 100644
--- a/Bookshelf/Combinator/Aviary.lean
+++ b/Common/Combinator/Aviary.lean
@@ -1,4 +1,4 @@
-/-! # Bookshelf.Combinator.Aviary
+/-! # Common.Combinator.Aviary
 
 A collection of combinator birds representable in Lean. Certain duplicators,
 e.g. mockingbirds, are not directly expressible since they would require
diff --git a/Common/LTuple.lean b/Common/LTuple.lean
new file mode 100644
index 0000000..8d046f3
--- /dev/null
+++ b/Common/LTuple.lean
@@ -0,0 +1 @@
+import Common.LTuple.Basic
\ No newline at end of file
diff --git a/Bookshelf/LTuple/Basic.lean b/Common/LTuple/Basic.lean
similarity index 99%
rename from Bookshelf/LTuple/Basic.lean
rename to Common/LTuple/Basic.lean
index c698b37..e6e2f46 100644
--- a/Bookshelf/LTuple/Basic.lean
+++ b/Common/LTuple/Basic.lean
@@ -1,6 +1,6 @@
 import Mathlib.Tactic.Ring
 
-/-! # Bookshelf.LTuple.Basic
+/-! # Common.LTuple.Basic
 
 The following is a representation of a (possibly empty) left-biased tuple. A
 left-biased `n`-tuple is defined recursively as follows:
diff --git a/Common/List.lean b/Common/List.lean
new file mode 100644
index 0000000..798f875
--- /dev/null
+++ b/Common/List.lean
@@ -0,0 +1 @@
+import Common.List.Basic
\ No newline at end of file
diff --git a/Bookshelf/List/Basic.lean b/Common/List/Basic.lean
similarity index 99%
rename from Bookshelf/List/Basic.lean
rename to Common/List/Basic.lean
index 194cea4..a2ca64f 100644
--- a/Bookshelf/List/Basic.lean
+++ b/Common/List/Basic.lean
@@ -1,7 +1,7 @@
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Tactic.NormNum
 
-/-! # Bookshelf.List.Basic
+/-! # Common.List.Basic
 
 Additional theorems and definitions useful in the context of `List`s.
 -/
diff --git a/Common/Real.lean b/Common/Real.lean
new file mode 100644
index 0000000..170f320
--- /dev/null
+++ b/Common/Real.lean
@@ -0,0 +1,7 @@
+import Common.Real.Basic
+import Common.Real.Function
+import Common.Real.Geometry
+import Common.Real.Int
+import Common.Real.Rational
+import Common.Real.Sequence
+import Common.Real.Set
diff --git a/Bookshelf/Real/Basic.lean b/Common/Real/Basic.lean
similarity index 93%
rename from Bookshelf/Real/Basic.lean
rename to Common/Real/Basic.lean
index c94c522..eb090c1 100644
--- a/Bookshelf/Real/Basic.lean
+++ b/Common/Real/Basic.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.Basic
 
-/-! # Bookshelf.Real.Basic
+/-! # Common.Real.Basic
 
 A collection of basic notational conveniences.
 -/
diff --git a/Common/Real/Function.lean b/Common/Real/Function.lean
new file mode 100644
index 0000000..c2a2a7a
--- /dev/null
+++ b/Common/Real/Function.lean
@@ -0,0 +1 @@
+import Common.Real.Function.Step
\ No newline at end of file
diff --git a/Bookshelf/Real/Function/Step.lean b/Common/Real/Function/Step.lean
similarity index 94%
rename from Bookshelf/Real/Function/Step.lean
rename to Common/Real/Function/Step.lean
index 1bb3f23..e718edd 100644
--- a/Bookshelf/Real/Function/Step.lean
+++ b/Common/Real/Function/Step.lean
@@ -1,7 +1,7 @@
-import Bookshelf.Real.Basic
-import Bookshelf.Real.Set.Partition
+import Common.Real.Basic
+import Common.Real.Set.Partition
 
-/-! # Bookshelf.Real.Function.Step
+/-! # Common.Real.Function.Step
 
 A characterization of step functions.
 -/
diff --git a/Common/Real/Geometry.lean b/Common/Real/Geometry.lean
new file mode 100644
index 0000000..46762f7
--- /dev/null
+++ b/Common/Real/Geometry.lean
@@ -0,0 +1,3 @@
+import Common.Real.Geometry.Area
+import Common.Real.Geometry.Basic
+import Common.Real.Geometry.Rectangle
\ No newline at end of file
diff --git a/Bookshelf/Real/Geometry/Area.lean b/Common/Real/Geometry/Area.lean
similarity index 97%
rename from Bookshelf/Real/Geometry/Area.lean
rename to Common/Real/Geometry/Area.lean
index 511b066..ccf2df3 100644
--- a/Bookshelf/Real/Geometry/Area.lean
+++ b/Common/Real/Geometry/Area.lean
@@ -1,7 +1,7 @@
-import Bookshelf.Real.Function.Step
-import Bookshelf.Real.Geometry.Rectangle
+import Common.Real.Function.Step
+import Common.Real.Geometry.Rectangle
 
-/-! # Bookshelf.Real.Geometry.Area
+/-! # Common.Real.Geometry.Area
 
 An axiomatic foundation for the concept of *area*. These axioms are those
 outlined in [^1].
diff --git a/Bookshelf/Real/Geometry/Basic.lean b/Common/Real/Geometry/Basic.lean
similarity index 96%
rename from Bookshelf/Real/Geometry/Basic.lean
rename to Common/Real/Geometry/Basic.lean
index 6eabafa..a4c7a1b 100644
--- a/Bookshelf/Real/Geometry/Basic.lean
+++ b/Common/Real/Geometry/Basic.lean
@@ -1,7 +1,8 @@
-import Bookshelf.Real.Basic
 import Mathlib.Data.Real.Sqrt
 
-/-! # Bookshelf.Real.Geometry.Basic
+import Common.Real.Basic
+
+/-! # Common.Real.Geometry.Basic
 
 A collection of useful definitions and theorems around geometry.
 -/
diff --git a/Bookshelf/Real/Geometry/Rectangle.lean b/Common/Real/Geometry/Rectangle.lean
similarity index 97%
rename from Bookshelf/Real/Geometry/Rectangle.lean
rename to Common/Real/Geometry/Rectangle.lean
index 8d86195..5ebc700 100644
--- a/Bookshelf/Real/Geometry/Rectangle.lean
+++ b/Common/Real/Geometry/Rectangle.lean
@@ -1,6 +1,6 @@
-import Bookshelf.Real.Geometry.Basic
+import Common.Real.Geometry.Basic
 
-/-! # Bookshelf.Real.Geometry.Rectangle
+/-! # Common.Real.Geometry.Rectangle
 
 A characterization of a rectangle. This follows the definition as outlined in
 [^1]. Note that a `Point` and a `LineSegment` are both considered rectangles,
diff --git a/Bookshelf/Real/Int.lean b/Common/Real/Int.lean
similarity index 56%
rename from Bookshelf/Real/Int.lean
rename to Common/Real/Int.lean
index 44c19db..446db2b 100644
--- a/Bookshelf/Real/Int.lean
+++ b/Common/Real/Int.lean
@@ -1,5 +1,10 @@
 import Mathlib.Data.Real.Basic
 
+/-! # Common.Real.Int
+
+Additional theorems and definitions useful in the context of integers.
+-/
+
 namespace Real
 
 /--
diff --git a/Bookshelf/Real/Rational.lean b/Common/Real/Rational.lean
similarity index 86%
rename from Bookshelf/Real/Rational.lean
rename to Common/Real/Rational.lean
index 5a1feaa..08fe988 100644
--- a/Bookshelf/Real/Rational.lean
+++ b/Common/Real/Rational.lean
@@ -1,6 +1,6 @@
-import Bookshelf.Real.Basic
+import Common.Real.Basic
 
-/-! # Bookshelf.Real.Rational
+/-! # Common.Real.Rational
 
 Additional theorems and definitions useful in the context of rational numbers.
 Most of these will likely be deleted once the corresponding functions in
diff --git a/Common/Real/Sequence.lean b/Common/Real/Sequence.lean
new file mode 100644
index 0000000..950b30a
--- /dev/null
+++ b/Common/Real/Sequence.lean
@@ -0,0 +1,2 @@
+import Common.Real.Sequence.Arithmetic
+import Common.Real.Sequence.Geometric
diff --git a/Bookshelf/Real/Sequence/Arithmetic.lean b/Common/Real/Sequence/Arithmetic.lean
similarity index 98%
rename from Bookshelf/Real/Sequence/Arithmetic.lean
rename to Common/Real/Sequence/Arithmetic.lean
index 4a8667f..469047e 100644
--- a/Bookshelf/Real/Sequence/Arithmetic.lean
+++ b/Common/Real/Sequence/Arithmetic.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.Basic
 
-/-! # Bookshelf.Real.Sequence.Arithmetic
+/-! # Common.Real.Sequence.Arithmetic
 
 A characterization of an arithmetic sequence, i.e. a sequence with a common
 difference between each term.
diff --git a/Bookshelf/Real/Sequence/Arithmetic.tex b/Common/Real/Sequence/Arithmetic.tex
similarity index 92%
rename from Bookshelf/Real/Sequence/Arithmetic.tex
rename to Common/Real/Sequence/Arithmetic.tex
index e415bd3..f183efc 100644
--- a/Bookshelf/Real/Sequence/Arithmetic.tex
+++ b/Common/Real/Sequence/Arithmetic.tex
@@ -3,7 +3,7 @@
 \input{../../../preamble}
 
 \newcommand{\link}[1]{\lean{../../..}
-  {Bookshelf/Real/Sequence/Arithmetic}
+  {Common/Real/Sequence/Arithmetic}
   {Real.Arithmetic.#1}
   {Real.Arithmetic.#1}
 }
diff --git a/Bookshelf/Real/Sequence/Geometric.lean b/Common/Real/Sequence/Geometric.lean
similarity index 98%
rename from Bookshelf/Real/Sequence/Geometric.lean
rename to Common/Real/Sequence/Geometric.lean
index 25076e8..50b2187 100644
--- a/Bookshelf/Real/Sequence/Geometric.lean
+++ b/Common/Real/Sequence/Geometric.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.Basic
 
-/-! # Bookshelf.Real.Sequence.Geometric
+/-! # Common.Real.Sequence.Geometric
 
 A characterization of a geometric sequence, i.e. a sequence with a common ratio
 between each term.
diff --git a/Bookshelf/Real/Sequence/Geometric.tex b/Common/Real/Sequence/Geometric.tex
similarity index 92%
rename from Bookshelf/Real/Sequence/Geometric.tex
rename to Common/Real/Sequence/Geometric.tex
index af35fc5..b048ef4 100644
--- a/Bookshelf/Real/Sequence/Geometric.tex
+++ b/Common/Real/Sequence/Geometric.tex
@@ -3,7 +3,7 @@
 \input{../../../preamble}
 
 \newcommand{\link}[1]{\lean{../../..}
-  {Bookshelf/Real/Sequence/Geometric}
+  {Common/Real/Sequence/Geometric}
   {Real.Geometric.#1}
   {Real.Geometric.#1}
 }
diff --git a/Common/Real/Set.lean b/Common/Real/Set.lean
new file mode 100644
index 0000000..e7b2fc3
--- /dev/null
+++ b/Common/Real/Set.lean
@@ -0,0 +1,3 @@
+import Common.Real.Set.Basic
+import Common.Real.Set.Interval
+import Common.Real.Set.Partition
\ No newline at end of file
diff --git a/Bookshelf/Real/Set/Basic.lean b/Common/Real/Set/Basic.lean
similarity index 96%
rename from Bookshelf/Real/Set/Basic.lean
rename to Common/Real/Set/Basic.lean
index 8b2f39f..af9f9e3 100644
--- a/Bookshelf/Real/Set/Basic.lean
+++ b/Common/Real/Set/Basic.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.Basic
 
-/-! # Bookshelf.Real.Set.Basic
+/-! # Common.Real.Set.Basic
 
 A collection of useful definitions and theorems regarding sets.
 -/
diff --git a/Bookshelf/Real/Set/Interval.lean b/Common/Real/Set/Interval.lean
similarity index 90%
rename from Bookshelf/Real/Set/Interval.lean
rename to Common/Real/Set/Interval.lean
index 6e297d1..fb14b0d 100644
--- a/Bookshelf/Real/Set/Interval.lean
+++ b/Common/Real/Set/Interval.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.Basic
 
-/-! # Bookshelf.Real.Set.Interval
+/-! # Common.Real.Set.Interval
 
 A syntactic description of the various types of continuous intervals permitted
 on the real number line.
diff --git a/Bookshelf/Real/Set/Partition.lean b/Common/Real/Set/Partition.lean
similarity index 96%
rename from Bookshelf/Real/Set/Partition.lean
rename to Common/Real/Set/Partition.lean
index e6e8ed2..d31c4ef 100644
--- a/Bookshelf/Real/Set/Partition.lean
+++ b/Common/Real/Set/Partition.lean
@@ -1,8 +1,9 @@
-import Bookshelf.List.Basic
-import Bookshelf.Real.Set.Interval
 import Mathlib.Data.List.Sort
 
-/-! # Bookshelf.Real.Set.Partition
+import Common.List.Basic
+import Common.Real.Set.Interval
+
+/-! # Common.Real.Set.Partition
 
 A description of a partition as defined in the context of stepwise functions.
 Refer to [^1] for more information.
diff --git a/Exercises/Apostol/Chapter_1_07.tex b/Exercises/Apostol/Chapter_1_07.tex
index 4b0b4a5..a057f13 100644
--- a/Exercises/Apostol/Chapter_1_07.tex
+++ b/Exercises/Apostol/Chapter_1_07.tex
@@ -6,8 +6,8 @@
 \input{../../preamble}
 \graphicspath{{./images/}}
 
-\newcommand{\larea}[2]{\lean{../..}{Bookshelf/Real/Geometry/Area}{#1}{#2}}
-\newcommand{\lrect}[2]{\lean{../..}{Bookshelf/Real/Geometry/Rectangle}{#1}{#2}}
+\newcommand{\larea}[2]{\lean{../..}{Common/Real/Geometry/Area}{#1}{#2}}
+\newcommand{\lrect}[2]{\lean{../..}{Common/Real/Geometry/Rectangle}{#1}{#2}}
 
 \begin{document}
 
diff --git a/Exercises/Apostol/Chapter_1_11.lean b/Exercises/Apostol/Chapter_1_11.lean
index 61497d9..d406cc6 100644
--- a/Exercises/Apostol/Chapter_1_11.lean
+++ b/Exercises/Apostol/Chapter_1_11.lean
@@ -1,6 +1,7 @@
-import Bookshelf.Real.Int
 import Mathlib.Data.Real.Basic
 
+import Common.Real.Int
+
 /-! # Exercises.Apostol.Exercises_1_11 -/
 
 namespace Exercises.Apostol.Exercises_1_11
diff --git a/Exercises/Apostol/Chapter_I_03.lean b/Exercises/Apostol/Chapter_I_03.lean
index 0718498..e5e4245 100644
--- a/Exercises/Apostol/Chapter_I_03.lean
+++ b/Exercises/Apostol/Chapter_I_03.lean
@@ -1,4 +1,4 @@
-import Bookshelf.Real.Set
+import Common.Real.Set
 
 /-! # Exercises.Apostol.Chapter_I_3
 
diff --git a/Exercises/Enderton/Chapter0.lean b/Exercises/Enderton/Chapter0.lean
index 5fb58a9..c852644 100644
--- a/Exercises/Enderton/Chapter0.lean
+++ b/Exercises/Enderton/Chapter0.lean
@@ -1,4 +1,4 @@
-import Bookshelf.LTuple.Basic
+import Common.LTuple.Basic
 
 /-! # Exercises.Enderton.Chapter0
 
diff --git a/lakefile.lean b/lakefile.lean
index 5db4891..6464469 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -16,7 +16,7 @@ require «doc-gen4» from git
 
 @[default_target]
 lean_lib «Bookshelf» {
-  roots := #[`Bookshelf, `Exercises]
+  roots := #[`Common, `Exercises]
 }
 
 /--