From e1a276f9188b4af21db01d36421f6a7a6a10643b Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 17 Apr 2024 00:45:37 +0200
Subject: [PATCH] Update 2-case2.tex

---
 blueprint/src/chapters/2-case2.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/blueprint/src/chapters/2-case2.tex b/blueprint/src/chapters/2-case2.tex
index 9cf942f..5c9cf83 100644
--- a/blueprint/src/chapters/2-case2.tex
+++ b/blueprint/src/chapters/2-case2.tex
@@ -747,9 +747,9 @@ \chapter{Case 2}
 
 \begin{lemma}
     \label{lmm:coprime_y_z}
-    \lean{Solution.coprime_y_z, def:Solution_x_y_z_w}
+    \lean{Solution.coprime_y_z}
     \leanok
-    \uses{def:Solution}
+    \uses{def:Solution, def:Solution_x_y_z_w}
     Let $S$ be a $solution$.\\\\
     Then $\gcd(y, z) = 1$.
 \end{lemma}
@@ -786,7 +786,7 @@ \chapter{Case 2}
     \label{lmm:x_mul_y_mul_z_eq_u_w_pow_three}
     \lean{Solution.x_mul_y_mul_z_eq_u_w_pow_three}
     \leanok
-    \uses{def:Solution}
+    \uses{def:Solution, def:Solution_x_y_z_w}
     Let $S=(a,b,c,u)$ be a $solution$.\\\\
     Then $x y z = u w^3$.
 \end{lemma}
@@ -873,7 +873,7 @@ \chapter{Case 2}
 
 \begin{lemma}
     \label{lmm:X_ne_zero}
-    \lean{Solution.X_ne_zero}
+    \lean{Solution.X_ne_zero, def:Solution_u1_u2_u3_u4_u5_X_Y_Z}
     \leanok
     \uses{def:Solution}
     Let $S$ be a $solution$.\\\\
@@ -891,7 +891,7 @@ \chapter{Case 2}
     \label{lmm:lambda_not_dvd_X}
     \lean{Solution.lambda_not_dvd_X}
     \leanok
-    \uses{def:Solution}
+    \uses{def:Solution, def:Solution_u1_u2_u3_u4_u5_X_Y_Z}
     Let $S$ be a $solution$.\\\\
     Then $\lambda \notdivides X$.
 \end{lemma}
@@ -909,7 +909,7 @@ \chapter{Case 2}
     \label{lmm:lambda_not_dvd_Y}
     \lean{Solution.lambda_not_dvd_Y}
     \leanok
-    \uses{def:Solution}
+    \uses{def:Solution, def:Solution_u1_u2_u3_u4_u5_X_Y_Z}
     Let $S$ be a $solution$.\\\\
     Then $\lambda \notdivides Y$.
 \end{lemma}