Structure projects in the same way.

first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean

@@ -1,6 +0,0 @@
-/-
-# References
-
-1. Fraleigh, John B. A First Course in Abstract Algebra, n.d.
--/
-import FirstCourseAbstractAlgebra.Exercises1

first-course-abstract-algebra/Fraleigh.lean

@@ -0,0 +1 @@
+import Fraleigh.Chapter1

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
+  _ = 0 + (-1) * I := by simp

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.

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»

mathematical-introduction-logic/Enderton.lean

@@ -0,0 +1 @@
+import Enderton.Chapter0

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

mathematical-introduction-logic/MathematicalIntroductionLogic.lean

@@ -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

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.

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"}}]}

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
 }

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

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

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

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

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

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

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

theorem-proving-in-lean/README.md

@@ -0,0 +1,3 @@
+# Theorem Proving in Lean
+
+Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.

theorem-proving-in-lean/TheoremProvingInLean.lean

@@ -1,6 +0,0 @@
-import TheoremProvingInLean.Exercises2
-import TheoremProvingInLean.Exercises3
-import TheoremProvingInLean.Exercises4
-import TheoremProvingInLean.Exercises5
-import TheoremProvingInLean.Exercises7
-import TheoremProvingInLean.Exercises8

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»