TileStructure.Forest.le_C7_1_6

lemma le_C7_1_6 (a4 : 4 ≤ a) :    D2_1_3 a * defaultA a ^ 5 * (2 : ℝ≥0∞) ^ (3 / a : ℝ) ≤ C7_1_6 a := by  simp_rw [D2_1_3, defaultA, C7_1_6, ENNReal.coe_pow, ENNReal.coe_ofNat, Nat.cast_pow,    Nat.cast_ofNat, ← pow_mul, ← pow_add]  calc    _ ≤ (2 : ℝ≥0∞) ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3 + a * 5) * 2 := by      refine mul_le_mul_right ?_ _      conv_rhs => rw [← ENNReal.rpow_one 2]      refine ENNReal.rpow_le_rpow_of_exponent_le one_le_two ?_      rw [div_le_one (by norm_cast; lia)]; norm_cast; lia    _ ≤ _ := by      rw [← pow_succ, add_assoc,        show (𝕔 + 3 + 𝕔 / 4) * a ^ 3 = (𝕔 + 2 + 𝕔 / 4) * a ^ 3 + a ^ 3 by ring]      gcongr; · exact one_le_two      calc        _ ≤ 4 * 4 * a := by lia        _ ≤ a * a * a := by gcongr        _ = _ := by ring