dense_cover

lemma dense_cover (k : ℕ) : volume (⋃ i ∈ 𝓒 (X := X) k, (i : Set X)) ≤ 2 ^ (k + 1) * volume G := by  classical  let M : Finset (Grid X) :=    { j | 2 ^ (-(k + 1 : ℕ) : ℤ) * volume (j : Set X) < volume (G ∩ j) }  have s₁ : ⋃ i ∈ 𝓒 (X := X) k, (i : Set X) ⊆ ⋃ i ∈ M, ↑i := by    simp_rw [𝓒]; intro q mq; rw [mem_iUnion₂] at mq ⊢; obtain ⟨i, hi, mi⟩ := mq    rw [aux𝓒, mem_sdiff, mem_setOf] at hi; obtain ⟨j, hj, mj⟩ := hi.1    use j, ?_, mem_of_mem_of_subset mi hj.1    simp only [M, Finset.mem_filter_univ]; exact mj  let M' := Grid.maxCubes M  have s₂ : ⋃ i ∈ M, (i : Set X) ⊆ ⋃ i ∈ M', ↑i := iUnion₂_mono' fun i mi ↦ by    obtain ⟨j, mj, hj⟩ := Grid.exists_maximal_supercube mi; use j, mj, hj.1  calc    _ ≤ volume (⋃ i ∈ M', (i : Set X)) := measure_mono (s₁.trans s₂)    _ ≤ ∑ i ∈ M', volume (i : Set X) := measure_biUnion_finset_le M' _    _ ≤ 2 ^ (k + 1) * ∑ j ∈ M', volume (G ∩ j) := by      rw [Finset.mul_sum]; refine Finset.sum_le_sum fun i hi ↦ ?_      replace hi : i ∈ M := Finset.mem_of_subset (Finset.filter_subset _ M) hi      rw [Finset.mem_filter_univ, ← ENNReal.rpow_intCast,        show (-(k + 1 : ℕ) : ℤ) = (-(k + 1) : ℝ) by simp, mul_comm,        ← ENNReal.lt_div_iff_mul_lt (by simp) (by simp), ENNReal.div_eq_inv_mul,        ← ENNReal.rpow_neg, neg_neg] at hi      exact_mod_cast hi.le    _ = 2 ^ (k + 1) * volume (⋃ j ∈ M', G ∩ j) := by      congr; refine (measure_biUnion_finset (fun _ mi _ mj hn ↦ ?_) (fun _ _ ↦ ?_)).symm      · exact ((Grid.maxCubes_pairwiseDisjoint mi mj hn).inter_right' G).inter_left' G      · exact measurableSet_G.inter coeGrid_measurable    _ ≤ _ := mul_le_mul_right (measure_mono (iUnion₂_subset fun _ _ ↦ inter_subset_left)) _