diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex
index 0708a85d..6f6bc7cc 100644
--- a/blueprint/src/chapter/main.tex
+++ b/blueprint/src/chapter/main.tex
@@ -5765,8 +5765,8 @@ \section{Proof of The Remaining Tiles Lemma}
 
     \begin{lemma}[thin scale impact]
         \label{thin-scale-impact}
-        % \leanok
-        % \lean{TileStructure.Forest.thin_scale_impact}
+        \leanok
+        \lean{TileStructure.Forest.thin_scale_impact}
         If $\fp \in \fT(\fu_2) \setminus \mathfrak{S}$ and $J \in \mathcal{J'}$ with $B(\scI(\fp)) \cap B(J) \ne \emptyset$, then
         $$
             \ps(\fp) \le s(J) + 2 - \frac{Zn}{202a^3}\,.