Tile.I12_le

lemma I12_le (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}    (hinter : (ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty)    (x1 : E p') (x2 : E p) :    I12 p p' g x1 x2 ≤    (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)) * ‖g x1‖ₑ * ‖g x2‖ₑ := by  apply (I12_le' hle x1 x2).trans  gcongr ?_ * _ * _  rw [pow_add 2 _ 1, pow_one, mul_comm _ 2, mul_assoc, mul_comm 2 (_ * _), mul_assoc]  gcongr  -- Now we need to use Lemma 6.2.3 to conclude this inequality.  have h623 := uncertainty (by lia) hle hinter x1.2 x2.2  rw [C6_2_3, ENNReal.coe_pow, ENNReal.coe_ofNat] at h623  have hneg : -(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹ < 0 :=    neg_neg_iff_pos.mpr (inv_pos.mpr (by norm_cast; nlinarith))  rw [← ENNReal.rpow_le_rpow_iff_of_neg hneg] at h623  have h0 : ((2 : ℝ≥0∞) ^ (8 * a)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) ≠ 0 := by simp  have h210 : (2 : ℝ≥0∞) ^ (1 : ℝ) ≠ 0 := by rw [ENNReal.rpow_one]; exact two_ne_zero  rw [ENNReal.mul_rpow_of_ne_top (by finiteness) (by finiteness), mul_comm,    ← ENNReal.le_div_iff_mul_le (.inl h0) (.inl (by finiteness))] at h623  apply h623.trans  rw [ENNReal.div_eq_inv_mul, mul_comm _ 2]  gcongr  conv_rhs => rw [← ENNReal.rpow_one (2 : ℝ≥0∞)]  rw [ENNReal.inv_le_iff_le_mul (fun _ ↦ h0) (fun _ ↦ h210), ← ENNReal.rpow_natCast 2,    ← ENNReal.rpow_mul, ← ENNReal.rpow_add _ _ two_ne_zero ENNReal.ofNat_ne_top]  exact ENNReal.one_le_rpow one_le_two (exp_ineq ha)