diff --git a/blueprint/src/chapter/FujisakiProject.tex b/blueprint/src/chapter/FujisakiProject.tex
index 5c0e4c10..d04da86a 100644
--- a/blueprint/src/chapter/FujisakiProject.tex
+++ b/blueprint/src/chapter/FujisakiProject.tex
@@ -70,6 +70,7 @@ \section{Enter the adeles}
   \label{AdeleRing.DivisionAlgebra.compact_quotient} If $D$ is a division algebra then
   the quotient $D^\times\backslash D_{\A}^{(1)}$
   with its quotient topology coming from $D_{\A}^{(1)}$, is compact.
+  \uses{DivisionAlgebra.units_cocompact}
 \end{theorem}
 
 The rest of this miniproject is devoted to a proof of this theorem.
@@ -116,6 +117,7 @@ \section{The proof}
   $\beta X\cap D^\times\not=\emptyset$.
   \end{lemma}
   \begin{proof}
+    \uses{E}
   Indeed by the previous lemma, the map $\beta E\to D\backslash D_{\A}$
   isn't injective, so there are distinct
   $\beta e_1,\beta e_2\in \beta E$ with $e_i\in E$ and
@@ -130,6 +132,7 @@ \section{The proof}
   $X\beta^{-1}\cap D^\times\not=\emptyset$.
 \end{lemma}
 \begin{proof}
+  \uses{E, addHaarScalarFactor.left_mul_eq_right_mul}
   Indeed, $\beta^{-1}\in D_{\A}^{(1)}$, and so left multiplication by $\beta^{-1}$
   doesn't change Haar measure on $D_{\A}$, so neither does right multiplication
   (by theorem~\ref{addHaarScalarFactor.left_mul_eq_right_mul}).
@@ -142,7 +145,9 @@ \section{The proof}
   \label{Y_meet_units_D}
   $Y\cap D^\times$ is finite.
 \end{lemma}
-\begin{proof} It suffices to prove that $Y\cap D$ is finite.
+\begin{proof}
+  \uses{E}
+  It suffices to prove that $Y\cap D$ is finite.
     But $D\subseteq D_{\A}$ is a discrete additive subgroup, and hence closed.
     And $Y\subseteq D_{\A}$ is compact.
     So $D\cap Y$ is compact and discrete, so finite.
@@ -152,14 +157,16 @@ \section{The proof}
 of $D_{\A}$, and define $K:= (T^{-1}.X) \times X\subset D_{\A}\times D_{\A}$,
 noting that $K$ is compact because $X$ is compact and $T$ is finite.
 
-\begin{lemma} For every $\beta\in D_{\A}^{(1)}$, there exists $b\in D^\times$
+\begin{lemma}
+  \label{exists_product}
+  For every $\beta\in D_{\A}^{(1)}$, there exists $b\in D^\times$
   and $\nu\in D_{\A}^{(1)}$ such that $\beta=b\nu$ and $(\nu,\nu^{-1})\in K.$
 \end{lemma}
 \begin{proof}
-
-  By an earlier lemma, $\beta X\cap D^\times\not=\emptyset$, and by another earlier lemma,
-  $X\beta^{-1}\cap D^\times\not=\emptyset$, so we can write $\beta x_1=b_1$
-  and $x_2\beta^{-1}=b_2$ with obvious notation.
+  \uses{E, X_meets_kernel, X_meets_kernel'}
+  By lemma~\ref{X_meets_kernel}, $\beta X\cap D^\times\not=\emptyset$,
+  and lemma~\ref{X_meets_kernel'}, $X\beta^{-1}\cap D^\times\not=\emptyset$,
+  so we can write $\beta x_1=b_1$ and $x_2\beta^{-1}=b_2$ with obvious notation.
 
   Multiplying, $x_2x_1=b_2b_1\in Y\cap D^\times=T$ (recall that $Y=X*X$ and $T=Y\cap D^\times$
   is finite); call this element $t$.
@@ -175,28 +182,28 @@ \section{The proof}
 We can now prove Fujisaki's theorem.
 
 \begin{theorem}
-  \label{DivisionAlegbra.units_cocompact}
+  \label{DivisionAlgebra.units_cocompact}
   $D^\times\backslash D_{\A}^{(1)}$ is compact.
 \end{theorem}
 \begin{proof}
+  \uses{DistribHaarChar.continuous, exists_product, Y_meet_units_D}
   Indeed, if $M$ is the preimage of $K$ under the map $D_{\A}^{(1)} \to D_{\A}\times D_{\A}$
   sending $\nu$ to $(\nu,\nu^{-1})$, then $M$ is a closed subspace
     of a compact
   space so it's compact (note that $\delta_{D_{\A}}$ is continuous,
   by theorem~\ref{DistribHaarChar.continuous}).
-  The previous lemma shows that $M$ surjects onto
+  Lemma~\ref{exists_product} shows that $M$ surjects onto
   $D^\times\backslash D_{\A}^{(1)}$ which is thus also compact.
 \end{proof}
 
 We note here a useful consequence.
 
 \begin{theorem}
-  \label{DivisionAlegbra.units_cocompact'}
+  \label{DivisionAlgebra.units_cocompact'}
   $D^\times\backslash(D\otimes_K\A_K^\infty)^\times$ is compact.
 \end{theorem}
-\begin{remark} In this generality the quotient might not be Hausdorff.
-\end{remark}
 \begin{proof}
+  \uses{DivisionAlgebra.units_cocompact}
   There's a natural map $\alpha$ from $D^\times\backslash D_{\A}^{(1)}$ to
   $D^\times\backslash (D\otimes_K \A_K^\infty)^\times$. We claim that it's
   surjective. Granted this claim, we are home, because if we put the quotient
@@ -216,3 +223,5 @@ \section{The proof}
   as multiplication by $x$ is just scaling by a factor of $x$ on $D_{\R}\cong\R^d$.
   In particular we can set $x=y^{1/d}$.
 \end{proof}
+\begin{remark} In this generality the quotient might not be Hausdorff.
+\end{remark}