Tile.volume_coeGrid_le

lemma volume_coeGrid_le {p : 𝔓 X} (x2 : E p) :    volume (𝓘 p : Set X) ≤ 2 ^ (3 * a) * volume (ball x2.1 (D ^ 𝔰 p)) := by  -- Inequality 6.2.30  have hdist : dist (𝔠 p) x2 < 4 * D ^ 𝔰 p :=    dist_comm (𝔠 p) x2 ▸ Grid_subset_ball (mem_of_subset_of_mem (fun _ ha ↦ ha.1) x2.prop)  -- Inclusion 6.2.31  have hsub : (𝓘 p : Set X) ⊆ ball x2 (8 * D ^ 𝔰 p) := by    refine Grid_subset_ball.trans fun x hx ↦ ?_    calc      _ ≤ dist x (𝔠 p) + dist (𝔠 p) x2 := dist_triangle ..      _ < 4 * D ^ 𝔰 p + 4 * D ^ 𝔰 p := add_lt_add hx hdist      _ = _ := by ring  apply (measure_mono hsub).trans  rw [show (8 : ℝ) = 2 ^ 3 by norm_num]  convert! measure_ball_two_le_same_iterate (μ := volume) x2.1 (D ^ 𝔰 p) 3 using 2  rw [mul_comm 3, pow_mul]; simp