one forgotten leanok

fpvandoorn · Sep 19, 2024 · 8016280 · 8016280
1 parent 1aaf327
commit 8016280
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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}\,.