TileStructure.Forest.local_dens1_tree_bound_exists

lemma local_dens1_tree_bound_exists (hu : u ∈ t) (hL : L ∈ 𝓛 (t u))    (hp₂ : ∃ p ∈ t u, ¬Disjoint ↑L (E p) ∧ 𝔰 p ≤ s L) :    volume (L ∩ G ∩ ⋃ p ∈ t u, E p) ≤ C7_3_2 a * dens₁ (t u) * volume (L : Set X) := by  obtain ⟨p, mp, dp, sp⟩ := hp₂; rw [disjoint_comm] at dp  replace dp : ¬Disjoint (𝓘 p : Set X) L := by contrapose! dp; exact dp.mono_left E_subset_𝓘  have lip := le_antisymm (le_of_mem_𝓛 hL mp dp) ((le_or_disjoint sp).resolve_right dp)  calc    _ ≤ volume (E₂ 9 p) := by      refine measure_mono fun x ⟨⟨mxL, mxG⟩, mxU⟩ ↦ ⟨⟨by apply lip ▸ mxL, mxG⟩, ?_⟩      rw [mem_iUnion₂] at mxU; obtain ⟨q, mq, hq⟩ := mxU; rw [smul_snd, mem_preimage]      have plq := lip ▸ le_of_mem_𝓛 hL mq (not_disjoint_iff.mpr ⟨x, E_subset_𝓘 hq, mxL⟩)      apply (@mem_ball' ..).mpr      calc        _ ≤ dist_(p) (𝒬 p) (𝒬 u) + dist_(p) (𝒬 u) (𝒬 q) + dist_(p) (𝒬 q) (Q x) :=          dist_triangle4 ..        _ ≤ dist_(p) (𝒬 p) (𝒬 u) + dist_(q) (𝒬 u) (𝒬 q) + dist_(q) (𝒬 q) (Q x) := by          gcongr <;> exact Grid.dist_mono plq        _ < 4 + 4 + 1 := by          gcongr          · exact t.dist_lt_four hu mp          · exact t.dist_lt_four' hu mq          · rw [← mem_ball']; exact subset_cball hq.2.1        _ = _ := by norm_num    _ ≤ 9 ^ a * dens₁ (t u) * volume (L : Set X) := by      rw [lip]      exact volume_E₂_le_dens₁_mul_volume (subset_lowerCubes mp) mp (by norm_num) le_rfl    _ ≤ _ := by      gcongr      rw [C7_3_2]      norm_cast      calc        _ ≤ 2 ^ (4 * a) := by rw [pow_mul]; gcongr; norm_num        _ ≤ _ := by          gcongr          · norm_num          · linarith [seven_le_c]          · apply Nat.le_pow (by norm_num)