From 8016280f84847d229278fe2be26fe63fb4d45ede Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 19 Sep 2024 15:55:06 +0200
Subject: [PATCH] one forgotten leanok

---
 blueprint/src/chapter/main.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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}\,.