TileStructure.Forest.estimate_C7_4_6

lemma estimate_C7_4_6 {a : ℕ} (n : ℕ) (ha : 4 ≤ a) :    C7_4_6 a n ≤ 2 ^ ((2 * 𝕔 + 9 + 𝕔 / 4) * a ^ 3) * 2 ^ (-(4 * n : ℝ)) := by  simp_rw [C7_4_6, C7_2_1, C7_6_2, C2_1_3, ← mul_assoc]  conv_lhs => enter [1, 1, 1, 2]; norm_cast  conv_lhs => enter [1, 1, 2, 2]; norm_cast  rw [← pow_add, ← pow_add]  simp_rw [NNReal.rpow_neg, ← div_eq_mul_inv]  gcongr 2 ^ ?_ / 2 ^ ?_  · exact one_le_two  · suffices 21 * a + 5 ≤ 2 * a ^ 3 by linarith    calc      _ ≤ 21 * a + 11 * 1 := by gcongr; norm_num      _ ≤ 21 * a + 11 * a := by gcongr; linarith      _ = 2 * 4 * 4 * a := by ring      _ ≤ 2 * a * a * a := by gcongr      _ = 2 * a ^ 3 := by ring  · exact one_le_two  · rw [← mul_rotate]; gcongr    rw [← mul_assoc, ← mul_rotate, ← mul_div_assoc, le_div_iff₀ (by positivity),      defaultκ, defaultZ, Nat.cast_pow, ← Real.rpow_natCast, Nat.cast_ofNat,      ← Real.rpow_add zero_lt_two, Nat.cast_mul, Nat.cast_ofNat, ← add_mul,      show 12 + -10 = (2 : ℝ) by norm_num]; norm_cast    induction a, ha using Nat.le_induction with    | base => ring_nf; linarith [seven_le_c]    | succ k lk ih =>      rw [mul_add_one, mul_add, mul_add_one, pow_add, show 2 ^ 2 = 3 + 1 by norm_num, mul_add_one,        add_mul, add_comm, add_mul]      gcongr ?_ + ?_      · calc          _ ≤ 4 * (4 * 𝕔 + 𝕔) := by gcongr; linarith [seven_le_c]          _ = 20 * 𝕔 := by ring          _ ≤ (2 ^ (2 * 4) * 3) * 𝕔 := by gcongr; norm_num          _ ≤ _ := by gcongr; norm_num      · convert! ih using 1        ring