From dbcd63ac65a686fbb6e062f1dbbaf0f88d9526ae Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 11 May 2023 08:04:29 -0600
Subject: [PATCH] Fix typos.

---
 README.md     | 2 +-
 lakefile.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 1977250..96658c7 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@ feasible, theorems are also formally proven in [Lean](https://leanprover.github.
 
 This project has absorbed [doc-gen4](https://github.com/leanprover/doc-gen4) to
 ease customization. In particular, the `DocGen4` module found in this project
-allows generating PDFs and including them into the navbar. To generate
+allows generating PDFs and including them in the navbar. To generate
 documentation and serve files locally, run the following:
 
 ```bash
diff --git a/lakefile.lean b/lakefile.lean
index fbee696..532bd7d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -31,7 +31,7 @@ require std4 from git
     "main"
 
 -- ========================================
--- Document Generator
+-- Documentation Generator
 -- ========================================
 
 lean_lib DocGen4