dens1_le_dens'

lemma dens1_le_dens' {k : ℕ} {P : Set (𝔓 X)} (hP : P ⊆ TilesAt k) : dens₁ P ≤ dens' k P := by  rw [dens₁, dens']; gcongr with p' mp' l hl  simp_rw [ENNReal.mul_iSup, iSup_le_iff, mul_div_assoc]; intro p mp sl  suffices p ∈ TilesAt k by    exact le_iSup_of_le p (le_iSup₂_of_le this sl (mul_le_mul' (by norm_cast) le_rfl))  simp_rw [TilesAt, mem_preimage, 𝓒, mem_sdiff, aux𝓒, mem_setOf]  constructor  · rw [mem_lowerCubes] at mp; obtain ⟨p'', mp'', lp''⟩ := mp    have hp'' := mem_of_mem_of_subset mp'' hP    simp_rw [TilesAt, mem_preimage, 𝓒, mem_sdiff, aux𝓒, mem_setOf] at hp''    obtain ⟨J, lJ, vJ⟩ := hp''.1; use J, lp''.trans lJ  · by_contra h; obtain ⟨J, lJ, vJ⟩ := h    have hp' := mem_of_mem_of_subset mp' hP    simp_rw [TilesAt, mem_preimage, 𝓒, mem_sdiff, aux𝓒, mem_setOf] at hp'    apply absurd _ hp'.2; use J, sl.1.trans lJ