Tile.bound_6_2_29

lemma bound_6_2_29 (ha : 4 ≤ a) {p p' : 𝔓 X} (x2 : E p) :    2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a + 1) *    (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) / volume (ball x2.1 (D ^ 𝔰 p)) ≤    C6_1_5 a *    (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) / volume (𝓘 p : Set X) := by  rw [mul_comm, mul_div_assoc, mul_comm (C6_1_5 a : ℝ≥0∞), mul_div_assoc]  refine mul_le_mul_right ?_ _  calc    _ = 2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 1) * 2 ^ (11 * a) * 2 ^ (-(3 : ℤ) * a) /        volume (ball x2.1 (D ^ 𝔰 p)) := by      simp_rw [← zpow_natCast, ← ENNReal.zpow_add two_ne_zero ENNReal.ofNat_ne_top]      congr; push_cast; ring    _ = 2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 1) * 2 ^ (11 * a) /        (2 ^ (3 * a) * volume (ball x2.1 (D ^ 𝔰 p))) := by      rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (by left; positivity) (by left; simp),        ← mul_assoc, ← zpow_natCast _ (3 * a), ← ENNReal.zpow_neg]      congr    _ ≤ C6_1_5 a / (2 ^ (3 * a) * volume (ball x2.1 (D ^ 𝔰 p))) := by      gcongr; exact ENNReal.coe_le_coe.mpr (C6_1_5_bound ha)    _ ≤ _ := by gcongr; exact volume_coeGrid_le _