TileStructure.Forest.estimate_C7_4_5

lemma estimate_C7_4_5 {a : ℕ} (n : ℕ) (ha : 4 ≤ a) :    C7_4_5 a n ≤ 2 ^ ((4 * 𝕔 + 11 + 4 * (𝕔 / 4)) * a ^ 3) * 2 ^ (-(4 * n : ℝ)) := by  simp_rw [C7_4_5, neg_div, NNReal.rpow_neg, ← div_eq_mul_inv]  gcongr _ / 2 ^ ?_  · exact one_le_two  · rw [mul_div_right_comm]; gcongr    rw [le_div_iff₀ (by positivity), defaultZ]; norm_cast    calc      _ = 8 * a * a * (a + 2) := by ring      _ ≤ 8 * a * a * (a + a) := by gcongr; lia      _ = 2 ^ 4 * a * a * a := by ring      _ ≤ 2 ^ a * 2 ^ a * 2 ^ a * 2 ^ a := by        gcongr; · exact one_le_two        all_goals exact Nat.lt_two_pow_self.le      _ ≤ _ := by simp_rw [← pow_add]; exact pow_le_pow_right' one_le_two (by linarith)