le_C1_0_2

lemma le_C1_0_2 (a4 : 4 ≤ a) (hq : q ∈ Ioc 1 2) :    C3_0_4 a q + 4 * C2_1_3 a * C2_0_6 (defaultA a) 1 q ≤ C1_0_2 a q := by  have : (1 : ℝ≥0) ≤ 2 := by norm_num  grw [C2_0_6_defaultA_one_le hq.1 (a := a)]  have : q / (q - 1) ≤ 2 / (q - 1) ^ 6 := by    gcongr    · have : 0 < q - 1 := tsub_pos_iff_lt.2 hq.1      positivity    · exact hq.2    · have : q - 1 = (q - 1) ^ 1 := by simp      conv_rhs => rw [this]      apply pow_le_pow_of_le_one (by simp) ?_ (by norm_num)      rw [tsub_le_iff_left]      exact hq.2.trans_eq (by norm_num)  grw [this]  simp only [C3_0_4, C2_1_3, C1_0_2, div_eq_mul_inv, ← mul_assoc, ← add_mul]  gcongr  rw [show (4 : ℝ≥0) = 2 ^ 2 by norm_num]  simp only [← pow_add, ← pow_succ]  apply add_le_pow_two le_rfl ?_ ?_  · ring_nf    suffices 2 + 4 * a ≤ a ^ 3 by lia    linarith [sixteen_times_le_cube a4]  · linarith [sixteen_times_le_cube a4]