TileStructure.Forest.volume_bound_of_Grid_lt

lemma volume_bound_of_Grid_lt {L L' : Grid X} (lL : L ≤ L') (sL : s L' = s L + 1) :    volume (L' : Set X) ≤ 2 ^ (𝕔 * a ^ 3 + 5 * a) * volume (L : Set X) := by  suffices volume (ball (c L') (4 * D ^ s L')) ≤      2 ^ (𝕔 * a ^ 3 + 5 * a) * volume (ball (c L) (D ^ s L / 4)) by    refine (le_trans ?_ this).trans ?_    · exact measure_mono Grid_subset_ball    · gcongr; exact ball_subset_Grid  have db : dist (c L) (c L') + 4 * D ^ s L' < 2 ^ (𝕔 * a ^ 2 + 5) * (D ^ s L / 4) := by    calc      _ < (4 : ℝ) * D ^ s L' + 4 * D ^ s L' := by        gcongr; rw [← mem_ball]        exact ((ball_subset_Grid.trans lL.1).trans Grid_subset_ball)          (mem_ball_self (by unfold defaultD; positivity))      _ = D * 2 ^ 5 * (D ^ s L / 4) := by        rw [← add_mul, show (4 : ℝ) + 4 = 2 ^ 5 / 4 by norm_num, sL, zpow_add_one₀ (by simp)]        ring      _ = _ := by congr 1; unfold defaultD; norm_cast; rw [pow_add]  convert measure_ball_le_of_dist_le' (μ := volume) (by simp) db.le  simp_rw [As, defaultA, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, Real.logb_pow,    Real.logb_self_eq_one one_lt_two, mul_one, Nat.ceil_natCast, ENNReal.coe_pow, ENNReal.coe_ofNat]  ring