From e06893d1f27e8758d638e4c3fc9e1bee3218abaf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Mar 2022 16:37:16 -0700
Subject: [PATCH] doc: proper TPIL link

---
 doc/SUMMARY.md | 2 +-
 doc/tpil.md    | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)
 create mode 100644 doc/tpil.md

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 88892f6a18..75f2fface4 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -5,7 +5,7 @@
 - [Setting Up Lean](./setup.md)
   - [Quickstart](./quickstart.md)
 
-# [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html)
+# [Theorem Proving in Lean](./tpil.md)
 
 # [Examples](./examples.md)
 
diff --git a/doc/tpil.md b/doc/tpil.md
new file mode 100644
index 0000000000..891d29ad38
--- /dev/null
+++ b/doc/tpil.md
@@ -0,0 +1,5 @@
+Theorem Proving in Lean
+=======================
+
+We strongly encourage you to read the book [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html).
+Many Lean users consider it to be the Lean Bible.