diff --git a/blueprint/src/chapters/2-case2.tex b/blueprint/src/chapters/2-case2.tex
index 292ff92..9cf942f 100644
--- a/blueprint/src/chapters/2-case2.tex
+++ b/blueprint/src/chapters/2-case2.tex
@@ -250,10 +250,6 @@ \chapter{Case 2}
     \lean{Solution.two_le_multiplicity}
     \leanok
     \uses{def:Solution}
-    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
-    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
-    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$ with multiplicity $n$.\\\\
     Then $2 \leq n$.
 \end{lemma}
@@ -273,7 +269,6 @@ \chapter{Case 2}
     Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S'=(a, b, c, u)$ be a $solution'$.\\\\
     Then $a^3 + b^3 = (a + b) (a + \eta b) (a + \eta^2 b)$.
 \end{lemma}
@@ -295,7 +290,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S'=(a, b, c, u)$ be a $solution'$.\\\\
     Then $(\lambda^2 \divides a + b) \lor (\lambda^2 \divides a +
     \eta b) \lor (\lambda^2 \divides a + \eta^2 b)$.
@@ -327,10 +321,6 @@ \chapter{Case 2}
     \lean{ex_dvd_a_add_b}
     \leanok
     \uses{def:Solution1}
-    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
-    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
-    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\\\
     Let $S'=(a, b, c, u)$ be a $solution'$.\\\\
     Then $\exists a_1,b_1 \in \cc{O}_k$ such that $S_1=(a_1,b_1,c,u)$ is a $solution$.
 \end{lemma}
@@ -389,7 +379,6 @@ \chapter{Case 2}
     Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     Then $a + \eta  b = (a + b) + \lambda  b$.
 \end{lemma}
@@ -409,7 +398,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     Then $\lambda \divides a + \eta  b$.
 \end{lemma}
@@ -430,7 +418,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     Then $\lambda \divides a + \eta^2  b$.
 \end{lemma}
@@ -452,7 +439,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     Then $\lambda^2 \notdivides a + \eta b$.
 \end{lemma}
@@ -477,7 +463,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     Then $\lambda^2 \notdivides a + \eta^2  b$.
 \end{lemma}
@@ -501,7 +486,6 @@ \chapter{Case 2}
     Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\\\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     Then $(\eta + 1)  (-\eta) = 1$.
 \end{lemma}
@@ -522,7 +506,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\
     Let $p \in \cc{O}_K$ be a prime such that $p \divides a+b$
     and $p \divides a+\eta  b$.\\\\
@@ -545,7 +528,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\\\
     Let $S=(a, b, c, u)$ be a $solution$.\\
     Let $p \in \cc{O}_K$ be a prime such that $p \divides a+b$
     and $p \divides a+\eta^2  b$.\\\\
@@ -568,7 +550,6 @@ \chapter{Case 2}
     Let $\zeta_3 \in K$ be any primitive third root of unity. \\
     Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
     Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
-    Let $u \in \cc{O}^\times_K$ be a unit. \\\\
     Let $S=(a, b, c, u)$ be a $solution$.\\
     Let $p \in \cc{O}_K$ be a prime such that $p \divides a+\eta b$
     and $p \divides a+\eta^2  b$.\\\\
@@ -585,6 +566,12 @@ \chapter{Case 2}
     %\lean{}
     \leanok
     \uses{def:Solution}
+    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
+    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
+    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+    Let $\zeta_3 \in K$ be any primitive third root of unity. \\
+    Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
+    Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
     Let $S=(a, b, c, u)$ be a $solution$.\\\\
     We define $x \in \cc{O}_K$ such that $a + b = \lambda^{3n-2}  x$.\\
     We define $y \in \cc{O}_K$ such that $a + \eta  b = \lambda  y$.\\
@@ -597,6 +584,12 @@ \chapter{Case 2}
     \lean{Solution.lambda_not_dvd_y}
     \leanok
     \uses{def:Solution}
+    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
+    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
+    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+    Let $\zeta_3 \in K$ be any primitive third root of unity. \\
+    Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
+    Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
     Let $S$ be a $solution$.\\\\
     Then $\lambda \notdivides y$.
 \end{lemma}
@@ -614,6 +607,12 @@ \chapter{Case 2}
     \lean{Solution.lambda_not_dvd_z}
     \leanok
     \uses{def:Solution}
+    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
+    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
+    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+    Let $\zeta_3 \in K$ be any primitive third root of unity. \\
+    Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
+    Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
     Let $S$ be a $solution$.\\\\
     Then $\lambda \notdivides z$.
 \end{lemma}
@@ -630,6 +629,12 @@ \chapter{Case 2}
     \lean{Solution.lambda_pow_dvd_a_add_b}
     \leanok
     \uses{def:Solution}
+    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
+    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
+    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+    Let $\zeta_3 \in K$ be any primitive third root of unity. \\
+    Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
+    Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
     Let $S=(a, b, c, u)$ be a $solution$ with multiplicity $n$.\\\\
     Then $\lambda^{3n -2} \divides a + b$.
 \end{lemma}
@@ -651,6 +656,12 @@ \chapter{Case 2}
     \lean{Solution.lambda_not_dvd_w}
     \leanok
     \uses{def:Solution}
+    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
+    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
+    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+    Let $\zeta_3 \in K$ be any primitive third root of unity. \\
+    Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
+    Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
     Let $S$ be a $solution$.\\\\
     Then $\lambda \notdivides w$.
 \end{lemma}
@@ -667,6 +678,12 @@ \chapter{Case 2}
     \lean{Solution.lambda_not_dvd_x}
     \leanok
     \uses{def:Solution}
+    Let $K = \Q(\zeta_3)$ be the third cyclotomic field. \\
+    Let $\cc{O}_K = \Z[\zeta_3]$ be the ring of integers of $K$. \\
+    Let $\cc{O}^\times_K$ be the group of units of $\cc{O}_K$. \\
+    Let $\zeta_3 \in K$ be any primitive third root of unity. \\
+    Let $\eta \in \cc{O}_K$ be the element corresponding to $\zeta_3 \in K$. \\
+    Let $\lambda \in \cc{O}_K$ be such that $\lambda = \eta -1$. \\
     Let $S$ be a $solution$.\\\\
     Then $\lambda \notdivides x$.
 \end{lemma}
@@ -688,7 +705,7 @@ \chapter{Case 2}
     \label{lmm:coprime_x_y}
     \lean{Solution.coprime_x_y}
     \leanok
-    \uses{def:Solution}
+    \uses{def:Solution, def:Solution_x_y_z_w}
     Let $S$ be a $solution$ with multiplicity $n$.\\\\
     Then $\gcd(x,y) = 1$.
 \end{lemma}
@@ -710,7 +727,7 @@ \chapter{Case 2}
     \label{lmm:coprime_x_z}
     \lean{Solution.coprime_x_z}
     \leanok
-    \uses{def:Solution}
+    \uses{def:Solution, def:Solution_x_y_z_w}
     Let $S$ be a $solution$.\\\\
     Then $\gcd(x,z) = 1$.
 \end{lemma}
@@ -730,7 +747,7 @@ \chapter{Case 2}
 
 \begin{lemma}
     \label{lmm:coprime_y_z}
-    \lean{Solution.coprime_y_z}
+    \lean{Solution.coprime_y_z, def:Solution_x_y_z_w}
     \leanok
     \uses{def:Solution}
     Let $S$ be a $solution$.\\\\