Add demo in Lean/blueprint and misc fixes

Reconstruction/Test.lean

@@ -1,3 +1,12 @@
 import Mathlib.Topology.Basic
 
 #check TopologicalSpace
+
+def one := 1
+
+def two := 2
+
+theorem one_plus_one_eq_two : one + one = two := by
+  rfl
+
+def one_plus_one_eq_two_with_def : Prop := one + one = two

blueprint/src/chapter/intro.tex

@@ -0,0 +1,39 @@
+\chapter{Introduction}
+\label{chap:intro}
+
+Formalisation of the proof of the 'germs' version of the reconstruction theorem.
+
+Below are some demos of how to refer to Lean definitions/theorems in the blueprint.
+
+\begin{definition}[One]
+\label{one}
+\lean{one}
+\leanok
+
+    one is 1.
+
+\end{definition}
+
+\begin{definition}[Two]
+\label{two}
+\lean{two}
+\leanok
+
+    two is 2.
+
+\end{definition}
+
+\begin{lemma}[One plus one is two]
+\label{one_plus_one_eq_two}
+\lean{one_plus_one_eq_two}
+\uses{one, two}
+\leanok
+
+one + one = two
+
+\end{lemma}
+
+\begin{proof}
+\leanok
+It is obvious.
+\end{proof}

blueprint/src/preamble/print.tex

@@ -14,3 +14,9 @@
 \newcommand{\proves}[1]{}
 \newcommand{\lean}[1]{}
 \newcommand{\leanok}{}
+
+% Define `ifplastex` so we can have complicated macros for PDF
+% and simplified macros for the website.
+% See http://plastex.github.io/plastex/plastex/sect0006.html
+\newif\ifplastex
+\plastexfalse

blueprint/src/print.tex

@@ -20,7 +20,7 @@
 \setmathfont[range=\varnothing]{Asana-Math.otf}
 \setmathfont[range=\pitchfork]{Asana-Math.otf}
 \setmathfont[range=\intprod]{Asana-Math.otf}
-\setmathfont[range=\int]{Latin Modern Math}
+\setmathfont[range=\int]{latinmodern-math.otf}
 
 \usepackage[nameinlink, capitalize]{cleveref}
 

blueprint/src/web.tex

@@ -8,7 +8,7 @@
 \usepackage{graphicx}
 \DeclareGraphicsExtensions{.svg,.png,.jpg}
 \usepackage[capitalize]{cleveref}
-\usepackage[showmore, dep_graph, project=../../]{blueprint}
+\usepackage[dep_graph, project=../../]{blueprint}
 
 \usepackage{tikz-cd}
 \usepackage{tikz}