diff --git a/.gitignore b/.gitignore
index 97ce1d0..4601aaf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,4 +8,9 @@
 *.fdb_latexmk
 *.fls
 *.log
-*.synctex.gz
\ No newline at end of file
+*.synctex.gz
+# Python virtual environment
+/.venv/
+# Lean blueprint
+/blueprint/lean_decls
+/blueprint/src/web.bbl
\ No newline at end of file
diff --git a/.vscode/settings.json b/.vscode/settings.json
index 61dc34b..271eb49 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,23 +1,22 @@
 {
     "files.exclude": {
-        "**/.git": true,
+        ".devcontainer": true,
+        ".docker": true,
         "**/.DS_Store": true,
-        "**/*.olean": true,
         "**/.DS_yml": true,
+        "**/.git": true,
         "**/.gitpod.yml": true,
         "**/.vscode": true,
-	".docker": true,
-	"build": true,
-	"html": true,
-	"lake-packages": true,
-	".gitignore": true,
-	"lake-manifest.json": true,
-	"lakefile.lean": true,
-	"lean-toolchain": true,
-	"mathematics_in_lean.pdf": true,
-    "LICENSE":true,
-    ".devcontainer":true,
-    "lean-tactics.tex":true
+        "**/*.olean": true,
+        "build": true,
+        "html": true,
+        "lake-manifest.json": true,
+        "lake-packages": true,
+        "lakefile.lean": true,
+        "lean-tactics.tex": true,
+        "lean-toolchain": true,
+        "LICENSE": true,
+        "mathematics_in_lean.pdf": true
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",
diff --git a/blueprint/src/chapter/plancherel.tex b/blueprint/src/chapter/plancherel.tex
index 45cdbbc..cf43028 100644
--- a/blueprint/src/chapter/plancherel.tex
+++ b/blueprint/src/chapter/plancherel.tex
@@ -296,21 +296,18 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 \end{corollary}
 \begin{proof}
   % \leanok
-  All of these follow immediately from the definition and the oberservation, that all operations (norms, sums, conjugation, $\ldots$) are continuous.
+  All of these follow immediately from the definition and the observation, that all operations (norms, sums, conjugation, $\ldots$) are continuous.
   For example, let $f\in L^2(V,E)$ and take an approximating sequence $(f_n)_n$ as before. Then
   $$\|\widehat f\|_2=\|\lim_{n\to\infty}\widehat f_n\|_2=\|\lim_{n\to\infty}\|\widehat f_n\|_2=\lim_{n\to\infty}\|f_n\|_2
   =\|\lim_{n\to\infty}f_n\|_2=\|f\|_2.$$
 \end{proof}
 
 \begin{corollary}
-  \label{thm:fourier-is-l2-linear}
-  \uses{thm:fourier2-properties} % the (list of) LaTeX labels of the lemmas that are used for this result
   \label{thm:fourier-is-l2-linear}
   \uses{thm:fourier2-properties} % the (list of) LaTeX labels of the lemmas that are used for this result
   \lean{MeasureTheory.fourierIntegralL2} % the full Lean name this corresponds to (can be a comma-separated list)
   \leanok % the *statement* of the lemma is formalized
   The Fourier transform induces a continuous linear map $L^2(V,E) \to L^2(V,E)$.
-  The Fourier transform induces a continuous linear map $L^2(V,E) \to L^2(V,E)$.
   \end{corollary}
   \begin{proof}
     % \uses{} % Put any results used in the proof but not in the statement here
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
index 3d30ada..9569b96 100644
--- a/blueprint/src/print.tex
+++ b/blueprint/src/print.tex
@@ -16,11 +16,11 @@
 \usepackage{mathtools}
 \usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
 \usepackage{fontspec}
-\setmathfont{Latin Modern Math}
-\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{Latin Modern Math}
+% \setmathfont[range=\varnothing]{Asana-Math.otf}
+% \setmathfont[range=\pitchfork]{Asana-Math.otf}
+% \setmathfont[range=\intprod]{Asana-Math.otf}
+% \setmathfont[range=\int]{Latin Modern Math}
 
 \usepackage[nameinlink, capitalize]{cleveref}