From ccaf8afe4540657d59f06b599cdf68480fc24e7e Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Wed, 31 Jul 2024 12:22:52 +0200
Subject: [PATCH] fix namespace

---
 Carleson/ForestOperator.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean
index e318e027..377991fa 100644
--- a/Carleson/ForestOperator.lean
+++ b/Carleson/ForestOperator.lean
@@ -87,6 +87,7 @@ lemma pairwiseDisjoint_𝓛 : (𝓛 G).PairwiseDisjoint (fun I ↦ (I : Set X))
 
 /-! ## Section 7.7 and Proposition 2.0.4 -/
 
+end TileStructure.Forest
 
 /-- The constant used in `forest_operator`.
 Has value `2 ^ (432 * a ^ 3 - (q - 1) / q * n)` in the blueprint. -/