diff --git a/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean b/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean
deleted file mode 100644
index 6c2bc9a..0000000
--- a/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-/-
-# References
-
-1. Fraleigh, John B. A First Course in Abstract Algebra, n.d.
--/
-import FirstCourseAbstractAlgebra.Exercises1
\ No newline at end of file
diff --git a/first-course-abstract-algebra/Fraleigh.lean b/first-course-abstract-algebra/Fraleigh.lean
new file mode 100644
index 0000000..d3e8abf
--- /dev/null
+++ b/first-course-abstract-algebra/Fraleigh.lean
@@ -0,0 +1 @@
+import Fraleigh.Chapter1
diff --git a/first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean b/first-course-abstract-algebra/Fraleigh/Chapter1.lean
similarity index 72%
rename from first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean
rename to first-course-abstract-algebra/Fraleigh/Chapter1.lean
index 11f39fc..f0f0df8 100644
--- a/first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean
+++ b/first-course-abstract-algebra/Fraleigh/Chapter1.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 1
 
-1. Fraleigh, John B. A First Course in Abstract Algebra, n.d.
+Introduction and Examples
 -/
 
 import Mathlib.Data.Complex.Basic
@@ -15,4 +15,4 @@ open HPow
 theorem ex1_1 : I^3 = 0 + (-1) * I := calc
   I^3
     = I * (I * hPow I 1) := rfl
-  _ = 0 + (-1) * I := by simp
\ No newline at end of file
+  _ = 0 + (-1) * I := by simp
diff --git a/first-course-abstract-algebra/README.md b/first-course-abstract-algebra/README.md
new file mode 100644
index 0000000..21cacc2
--- /dev/null
+++ b/first-course-abstract-algebra/README.md
@@ -0,0 +1,3 @@
+# A First Course in Abstract Algebra
+
+Fraleigh, John B. A First Course in Abstract Algebra, n.d.
diff --git a/first-course-abstract-algebra/lakefile.lean b/first-course-abstract-algebra/lakefile.lean
index 2c7a6f3..847a260 100644
--- a/first-course-abstract-algebra/lakefile.lean
+++ b/first-course-abstract-algebra/lakefile.lean
@@ -9,6 +9,4 @@ require mathlib from git
     "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"
 
 @[default_target]
-lean_lib «FirstCourseAbstractAlgebra» {
-  -- add library configuration options here
-}
+lean_lib «fraleigh»
diff --git a/mathematical-introduction-logic/Enderton.lean b/mathematical-introduction-logic/Enderton.lean
new file mode 100644
index 0000000..c336653
--- /dev/null
+++ b/mathematical-introduction-logic/Enderton.lean
@@ -0,0 +1 @@
+import Enderton.Chapter0
diff --git a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean b/mathematical-introduction-logic/Enderton/Chapter0.lean
similarity index 98%
rename from mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean
rename to mathematical-introduction-logic/Enderton/Chapter0.lean
index 57e0c98..f0e95e2 100644
--- a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean
+++ b/mathematical-introduction-logic/Enderton/Chapter0.lean
@@ -1,8 +1,7 @@
 /-
-# References
+Chapter 0
 
-1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
-   Harcourt/Academic Press, 2001.
+Useful Facts About Sets
 -/
 
 import Bookshelf.Tuple
diff --git a/mathematical-introduction-logic/MathematicalIntroductionLogic.lean b/mathematical-introduction-logic/MathematicalIntroductionLogic.lean
deleted file mode 100644
index d34aba4..0000000
--- a/mathematical-introduction-logic/MathematicalIntroductionLogic.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-/-
-# References
-
-1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
-   Harcourt/Academic Press, 2001.
--/
-import MathematicalIntroductionLogic.Chapter0
diff --git a/mathematical-introduction-logic/README.md b/mathematical-introduction-logic/README.md
new file mode 100644
index 0000000..abcd6ee
--- /dev/null
+++ b/mathematical-introduction-logic/README.md
@@ -0,0 +1,4 @@
+# A Mathematical Introduction to Logic
+
+Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
+Harcourt/Academic Press, 2001.
diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json
index a6ef150..123a66f 100644
--- a/mathematical-introduction-logic/lake-manifest.json
+++ b/mathematical-introduction-logic/lake-manifest.json
@@ -5,24 +5,24 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87",
+    "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a",
     "name": "mathlib",
-    "inputRev?": "7e974fd3806866272e9f6d9e44fa04c210a21f87"}},
+    "inputRev?": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+    "rev": "7ae096b232087096ff0243a2b70d32720d2621ae",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6",
+    "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7",
+    "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/mathematical-introduction-logic/lakefile.lean b/mathematical-introduction-logic/lakefile.lean
index 9ea98f4..6ead34c 100644
--- a/mathematical-introduction-logic/lakefile.lean
+++ b/mathematical-introduction-logic/lakefile.lean
@@ -6,6 +6,6 @@ package «mathematical-introduction-logic»
 require Bookshelf from "../bookshelf"
 
 @[default_target]
-lean_lib «MathematicalIntroductionLogic» {
+lean_lib «enderton» {
   -- add library configuration options here
 }
diff --git a/theorem-proving-in-lean/Avigad.lean b/theorem-proving-in-lean/Avigad.lean
new file mode 100644
index 0000000..478fb85
--- /dev/null
+++ b/theorem-proving-in-lean/Avigad.lean
@@ -0,0 +1,6 @@
+import Avigad.Chapter2
+import Avigad.Chapter3
+import Avigad.Chapter4
+import Avigad.Chapter5
+import Avigad.Chapter7
+import Avigad.Chapter8
diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean b/theorem-proving-in-lean/Avigad/Chapter2.lean
similarity index 97%
rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean
rename to theorem-proving-in-lean/Avigad/Chapter2.lean
index 13edbaa..37066f8 100644
--- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean
+++ b/theorem-proving-in-lean/Avigad/Chapter2.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 2
 
-1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+Dependent Type Theory
 -/
 
 -- Exercise 1
diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean b/theorem-proving-in-lean/Avigad/Chapter3.lean
similarity index 98%
rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean
rename to theorem-proving-in-lean/Avigad/Chapter3.lean
index 0f69765..47b465d 100644
--- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean
+++ b/theorem-proving-in-lean/Avigad/Chapter3.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 3
 
-1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+Propositions and Proofs
 -/
 
 -- Exercise 1
diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean b/theorem-proving-in-lean/Avigad/Chapter4.lean
similarity index 99%
rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean
rename to theorem-proving-in-lean/Avigad/Chapter4.lean
index d016adc..6768087 100644
--- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean
+++ b/theorem-proving-in-lean/Avigad/Chapter4.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 4
 
-1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+Quantifiers and Equality
 -/
 
 -- Exercise 1
diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean b/theorem-proving-in-lean/Avigad/Chapter5.lean
similarity index 99%
rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean
rename to theorem-proving-in-lean/Avigad/Chapter5.lean
index e269ec1..1698e11 100644
--- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean
+++ b/theorem-proving-in-lean/Avigad/Chapter5.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 5
 
-1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+Tactics
 -/
 
 -- Exercise 1
diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean b/theorem-proving-in-lean/Avigad/Chapter7.lean
similarity index 99%
rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean
rename to theorem-proving-in-lean/Avigad/Chapter7.lean
index b5dde0f..032e5f9 100644
--- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean
+++ b/theorem-proving-in-lean/Avigad/Chapter7.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 7
 
-1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+Inductive Types
 -/
 
 -- Exercise 1
diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean b/theorem-proving-in-lean/Avigad/Chapter8.lean
similarity index 98%
rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean
rename to theorem-proving-in-lean/Avigad/Chapter8.lean
index 934b394..0ae3c31 100644
--- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean
+++ b/theorem-proving-in-lean/Avigad/Chapter8.lean
@@ -1,7 +1,7 @@
 /-
-# References
+Chapter 8
 
-1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+Induction and Recursion
 -/
 
 -- Exercise 1
diff --git a/theorem-proving-in-lean/README.md b/theorem-proving-in-lean/README.md
new file mode 100644
index 0000000..e370109
--- /dev/null
+++ b/theorem-proving-in-lean/README.md
@@ -0,0 +1,3 @@
+# Theorem Proving in Lean
+
+Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
diff --git a/theorem-proving-in-lean/TheoremProvingInLean.lean b/theorem-proving-in-lean/TheoremProvingInLean.lean
deleted file mode 100644
index 277ec5e..0000000
--- a/theorem-proving-in-lean/TheoremProvingInLean.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import TheoremProvingInLean.Exercises2
-import TheoremProvingInLean.Exercises3
-import TheoremProvingInLean.Exercises4
-import TheoremProvingInLean.Exercises5
-import TheoremProvingInLean.Exercises7
-import TheoremProvingInLean.Exercises8
\ No newline at end of file
diff --git a/theorem-proving-in-lean/lakefile.lean b/theorem-proving-in-lean/lakefile.lean
index d989b0a..a5dd762 100644
--- a/theorem-proving-in-lean/lakefile.lean
+++ b/theorem-proving-in-lean/lakefile.lean
@@ -4,4 +4,4 @@ open Lake DSL
 package «theorem-proving-in-lean»
 
 @[default_target]
-lean_lib «TheoremProvingInLean»
+lean_lib «avigad»