Use `Bookshelf` instead of `Common`.

common/Common/List.lean

@@ -1 +0,0 @@
-import Common.List.Basic

common/Common/Real.lean

@@ -1,5 +0,0 @@
-import Common.Real.Basic
-import Common.Real.Function
-import Common.Real.Geometry
-import Common.Real.Sequence
-import Common.Real.Set

common/Common/Real/Function.lean

@@ -1 +0,0 @@
-import Common.Real.Function.Step

common/Common/Real/Geometry.lean

@@ -1,2 +0,0 @@
-import Common.Real.Geometry.Basic
-import Common.Real.Geometry.Rectangle

common/Common/Real/Sequence.lean

@@ -1,2 +0,0 @@
-import Common.Real.Sequence.Arithmetic
-import Common.Real.Sequence.Geometric

common/Common/Real/Set.lean

@@ -1,3 +0,0 @@
-import Common.Real.Set.Basic
-import Common.Real.Set.Interval
-import Common.Real.Set.Partition

first-course-abstract-algebra/lake-manifest.json

@@ -1,7 +1,8 @@
 {"version": 4,
  "packagesDir": "lake-packages",
  "packages":
- [{"git":
+ [{"path": {"name": "Bookshelf", "dir": "./../shared"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
     "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a",
@@ -24,5 +25,4 @@
     "subDir?": null,
     "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
     "name": "std",
-    "inputRev?": "main"}},
+    "inputRev?": "main"}}]}
-  {"path": {"name": "Common", "dir": "./../common"}}]}

first-course-abstract-algebra/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package «first-course-abstract-algebra»
 
-require Common from "../common"
+require Bookshelf from "../shared"
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @
     "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"

mathematical-introduction-logic/Enderton/Chapter0.lean

@@ -4,15 +4,15 @@ Chapter 0
 Useful Facts About Sets
 -/
 
-import Common.Tuple
+import Bookshelf.Tuple
 
 /--
-The following describes a so-called "generic" tuple. Like in `Common.Tuple`, an
+The following describes a so-called "generic" tuple. Like in `Bookshelf.Tuple`,
-`n`-tuple is defined recursively like so:
+an `n`-tuple is defined recursively like so:
 
   `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
 
-Unlike `Common.Tuple`, a "generic" tuple bends the syntax above further. For
+Unlike `Bookshelf.Tuple`, a "generic" tuple bends the syntax above further. For
 example, both tuples above are equivalent to:
 
   `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩`
@@ -20,7 +20,7 @@ example, both tuples above are equivalent to:
 for some `1 ≤ m ≤ n`. This distinction is purely syntactic, but necessary to
 prove certain theorems found in [1] (e.g. `lemma_0a`).
 
-In general, prefer `Common.Tuple`.
+In general, prefer `Bookshelf.Tuple`.
 -/
 inductive XTuple : (α : Type u) → (size : Nat × Nat) → Type u where
   | nil : XTuple α (0, 0)

mathematical-introduction-logic/lake-manifest.json

@@ -1,7 +1,8 @@
 {"version": 4,
  "packagesDir": "lake-packages",
  "packages":
- [{"git":
+ [{"path": {"name": "Bookshelf", "dir": "./../shared"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
     "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a",
@@ -24,5 +25,4 @@
     "subDir?": null,
     "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
     "name": "std",
-    "inputRev?": "main"}},
+    "inputRev?": "main"}}]}
-  {"path": {"name": "Common", "dir": "./../common"}}]}

mathematical-introduction-logic/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package «mathematical-introduction-logic»
 
-require Common from "../common"
+require Bookshelf from "../shared"
 
 @[default_target]
 lean_lib «enderton»

one-variable-calculus/Apostol/Chapter_1_6.lean

@@ -3,8 +3,8 @@ Chapter 1.6
 
 The concept of area as a set function
 -/
-import Common.Real.Function.Step
+import Bookshelf.Real.Function.Step
-import Common.Real.Geometry.Rectangle
+import Bookshelf.Real.Geometry.Rectangle
 
 namespace Real
 

one-variable-calculus/Apostol/Chapter_I_3.lean

@@ -3,7 +3,7 @@ Chapter I 3
 
 A Set of Axioms for the Real-Number System
 -/
-import Common.Real.Set
+import Bookshelf.Real.Set
 
 #check Archimedean
 #check Real.exists_isLUB

one-variable-calculus/lake-manifest.json

@@ -1,7 +1,8 @@
 {"version": 4,
  "packagesDir": "lake-packages",
  "packages":
- [{"git":
+ [{"path": {"name": "Bookshelf", "dir": "./../shared"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
     "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a",
@@ -24,5 +25,4 @@
     "subDir?": null,
     "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
     "name": "std",
-    "inputRev?": "main"}},
+    "inputRev?": "main"}}]}
-  {"path": {"name": "Common", "dir": "./../common"}}]}

one-variable-calculus/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package «one-variable-calculus»
 
-require Common from "../common"
+require Bookshelf from "../shared"
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @
     "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"

shared/Bookshelf/List.lean

@@ -0,0 +1 @@
+import Bookshelf.List.Basic

shared/Bookshelf/Real.lean

@@ -0,0 +1,5 @@
+import Bookshelf.Real.Basic
+import Bookshelf.Real.Function
+import Bookshelf.Real.Geometry
+import Bookshelf.Real.Sequence
+import Bookshelf.Real.Set

shared/Bookshelf/Real/Function.lean

@@ -0,0 +1 @@
+import Bookshelf.Real.Function.Step

shared/Bookshelf/Real/Function/Step.lean

@@ -1,8 +1,8 @@
 import Mathlib.Data.Fin.Basic
 import Mathlib.Tactic.NormNum
 
-import Common.Real.Basic
+import Bookshelf.Real.Basic
-import Common.Real.Set.Partition
+import Bookshelf.Real.Set.Partition
 
 namespace Real.Function
 
@@ -35,4 +35,4 @@ def set_def (f : Step) : Set ℝ² := sorry
 
 -- TODO: Fill out
 
-end Real.Function.Step
+end Real.Function.Step

shared/Bookshelf/Real/Geometry.lean

@@ -0,0 +1,2 @@
+import Bookshelf.Real.Geometry.Basic
+import Bookshelf.Real.Geometry.Rectangle

shared/Bookshelf/Real/Geometry/Basic.lean

@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.Sqrt
 
-import Common.Real.Basic
+import Bookshelf.Real.Basic
 
 namespace Real
 
@@ -47,4 +47,4 @@ theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := b
   conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)]
   exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
 
-end Real
+end Real

shared/Bookshelf/Real/Geometry/Rectangle.lean

@@ -1,4 +1,4 @@
-import Common.Real.Geometry.Basic
+import Bookshelf.Real.Geometry.Basic
 
 namespace Real
 
@@ -41,4 +41,4 @@ Computes the height of a `Rectangle`.
 noncomputable def height (r : Rectangle) : ℝ :=
   dist r.bottom_left r.bottom_right
 
-end Real.Rectangle
+end Real.Rectangle

shared/Bookshelf/Real/Sequence.lean

@@ -0,0 +1,2 @@
+import Bookshelf.Real.Sequence.Arithmetic
+import Bookshelf.Real.Sequence.Geometric

shared/Bookshelf/Real/Set.lean

@@ -0,0 +1,3 @@
+import Bookshelf.Real.Set.Basic
+import Bookshelf.Real.Set.Interval
+import Bookshelf.Real.Set.Partition

shared/Bookshelf/Real/Set/Partition.lean

@@ -1,5 +1,5 @@
-import Common.List.Basic
+import Bookshelf.List.Basic
-import Common.Real.Set.Interval
+import Bookshelf.Real.Set.Interval
 
 namespace Real
 
@@ -42,4 +42,4 @@ instance : Membership ℝ Partition where
 
 end Partition
 
-end Real
+end Real

shared/lakefile.lean

@@ -1,11 +1,11 @@
 import Lake
 open Lake DSL
 
-package «Common»
+package «Bookshelf»
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @
     "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"
 
 @[default_target]
-lean_lib «Common»
+lean_lib «Bookshelf»