From 1c988dc9e9f5f7f62321163d637457c8e8ac1704 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 10 Aug 2023 11:31:14 -0600
Subject: [PATCH] Update mathlib4 links to Lean's hosted index instead.

---
 Bookshelf/Apostol.tex        |  2 +-
 Bookshelf/Enderton/Logic.tex |  2 +-
 Bookshelf/Enderton/Set.tex   |  2 +-
 Common/Real/Sequence.tex     |  2 +-
 preamble.tex                 | 43 ++++++++++++++++++------------------
 5 files changed, 26 insertions(+), 25 deletions(-)

diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex
index 9d57e83..ccb00c2 100644
--- a/Bookshelf/Apostol.tex
+++ b/Bookshelf/Apostol.tex
@@ -4,7 +4,7 @@
 \graphicspath{{./Apostol/images/}}
 
 \input{../preamble}
-\makeleancommands{..}
+\makecode{..}
 
 \begin{document}
 
diff --git a/Bookshelf/Enderton/Logic.tex b/Bookshelf/Enderton/Logic.tex
index c7f06b3..caebefb 100644
--- a/Bookshelf/Enderton/Logic.tex
+++ b/Bookshelf/Enderton/Logic.tex
@@ -1,7 +1,7 @@
 \documentclass{report}
 
 \input{../../preamble}
-\makeleancommands{../..}
+\makecode{../..}
 
 \begin{document}
 
diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index fb551d3..fbed7d7 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -4,7 +4,7 @@
 \graphicspath{{./Set/images/}}
 
 \input{../../preamble}
-\makeleancommands{../..}
+\makecode{../..}
 
 \newcommand{\pair}[1]{\left< #1 \right>}
 \newcommand{\ineq}{\,\mathop{\underline{\in}}\,}
diff --git a/Common/Real/Sequence.tex b/Common/Real/Sequence.tex
index 40c4738..a90f62d 100644
--- a/Common/Real/Sequence.tex
+++ b/Common/Real/Sequence.tex
@@ -1,7 +1,7 @@
 \documentclass{article}
 
 \input{../../preamble}
-\makeleancommands{../..}
+\makecode{../..}
 
 \begin{document}
 
diff --git a/preamble.tex b/preamble.tex
index 8eaf150..579cd5a 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -44,43 +44,44 @@
   \label{#1}%
   \hypertarget{#1}{}}
 
-% Denote if working with a predefined statement/theorem or a custom one.
-\newcommand\@leanlink[4]{%
+% Links to theorems/statements/etc. that can be found in Mathlib4's index.
+\newcommand\@leanlink[3]{%
   \textcolor{BlueViolet}{\raisebox{-4.5pt}{%
     \tikz{\draw (0, 0) node[yscale=-1,xscale=1] {\faFont};}}{-\;}}%
-  \href{#1/#2.html\##3}{\color{BlueViolet}{#4}}}
+  \href{https://leanprover-community.github.io/mathlib4_docs/#1.html\##2}%
+  {\color{BlueViolet}{#3}}}
+
+\newcommand\lean[2]{%
+  \noindent\@leanlink{#1}{#2}{#2}}
+\WithSuffix\newcommand\lean*[2]{%
+  \vspace{6pt}\lean{#1}{#2}}
+
+\newcommand\leanp[3]{%
+  \noindent\@leanlink{#1}{#2}{#3}}
+\WithSuffix\newcommand\leanp*[3]{%
+  \vspace{6pt}\leanp{#1}{#2}{#3}}
+
+% Links to theorems/statements/etc. found in custom index.
 \newcommand\@codelink[4]{%
   \textcolor{MidnightBlue}{\raisebox{-4.5pt}{%
     \tikz{\draw (0, 0) node[xshift=8pt] {\faCodeBranch};}}{-\;}}%
-  \href{#1/#2.html\##3}{\color{MidnightBlue}{#4}}}
+  \href{#1/#2.html\##3}%
+  {\color{MidnightBlue}{#4}}}
 
-% Reference to an anchor of generated Lean documentation.
-\newcommand\leanref[3]{%
-  \@leanlink{#1}{#2}{#3}{#3}}
 \newcommand\coderef[3]{%
   \@codelink{#1}{#2}{#3}{#3}}
-\newcommand\leanpref[4]{%
-  \@leanlink{#1}{#2}{#3}{#4}}
 \newcommand\codepref[4]{%
   \@codelink{#1}{#2}{#3}{#4}}
 
-% Macro to build all Lean related commands relative to a specified directory.
-\newcommand\makeleancommands[1]{%
-  \newcommand\lean[2]{%
-    \noindent\leanref{#1}{##1}{##2}}
-  \WithSuffix\newcommand\lean*[2]{%
-    \vspace{6pt}\noindent\leanref{#1}{##1}{##2}}
-
+% Macro to build our `code` commands relative to a given directory. For
+% instance, we expect to have invocation `\makecode{..}` if the TeX file exists
+% one directory deep from the root of our project..
+\newcommand\makecode[1]{%
   \newcommand\code[2]{%
     \noindent\coderef{#1}{##1}{##2}}
   \WithSuffix\newcommand\code*[2]{%
     \vspace{6pt}\noindent\coderef{#1}{##1}{##2}}
 
-  \newcommand\leanp[3]{%
-    \noindent\leanpref{#1}{##1}{##2}{##3}}
-  \WithSuffix\newcommand\leanp*[3]{%
-    \vspace{6pt}\noindent\leanpref{#1}{##1}{##2}{##3}}
-
   \newcommand\codep[3]{%
     \noindent\codepref{#1}{##1}{##2}{##3}}
   \WithSuffix\newcommand\codep*[3]{%