dens'_le_of_mem_𝔓pos

lemma dens'_le_of_mem_𝔓pos (h : p ∈ 𝔓pos (X := X)) : dens' k {p} ≤ 2 ^ (-k : ℤ) := by  simp_rw [dens', mem_singleton_iff, iSup_iSup_eq_left, iSup_le_iff]; intro l hl p' mp' sl  have vpos : 0 < volume (𝓘 p' : Set X) := by    refine lt_of_lt_of_le ?_ (measure_mono sl.1.1)    rw [𝔓pos, mem_setOf, inter_assoc] at h; exact h.trans_le (measure_mono inter_subset_left)  rw [ENNReal.div_le_iff vpos.ne' volume_coeGrid_lt_top.ne]  calc    _ ≤ volume (E₂ l p') := by      nth_rw 2 [← one_mul (volume _)]; apply mul_le_mul_left      rw [show 1 = (l : ℝ≥0∞) ^ (0 : ℤ) by simp]; apply ENNReal.zpow_le_of_le      · rw [ENNReal.one_le_coe_iff]; exact one_le_two.trans hl      · linarith [four_le_a X]    _ ≤ _ := by      have E : E₂ l p' ⊆ 𝓘 p' ∩ G := inter_subset_left      rw [TilesAt, mem_preimage, 𝓒, mem_sdiff] at mp'; replace mp' := mp'.2      rw [aux𝓒, mem_setOf] at mp'; push Not at mp'; specialize mp' (𝓘 p') le_rfl      rw [inter_comm] at E; exact (measure_mono E).trans mp'