Antichain.C2_0_6_q₆_le

lemma C2_0_6_q₆_le (a4 : 4 ≤ a) : C2_0_6 (defaultA a) (q₆ a).toNNReal 2 ≤ 2 ^ (a + 2) := by  rw [C2_0_6, Real.coe_toNNReal _ (q₆_pos a4).le]  nth_rw 1 [show (2 : ℝ≥0) = (2 : ℝ).toNNReal by simp]  rw [← Real.toNNReal_div zero_le_two, CMB_def, C_realInterpolation, C_realInterpolation_ENNReal]  simp_rw [ENNReal.top_ne_one, ENNReal.one_lt_top, lt_self_iff_false, ite_true, ite_false,    ENNReal.coe_one, ENNReal.one_rpow, zero_mul, add_zero, NNReal.coe_one, one_mul, mul_one,    ENNReal.toReal_inv, ENNReal.coe_toReal, ENNReal.toReal_one]  have dvg1 : 1 < 2 / q₆ a :=    (one_lt_div (q₆_pos a4)).mpr ((q₆_le_superparticular a4).trans_lt (by norm_num))  have dvpos : 0 < 2 / q₆ a := zero_lt_one.trans dvg1  have ipos : 0 < (2 / q₆ a - 1)⁻¹ := by rwa [inv_pos, sub_pos]  rw [Real.coe_toNNReal _ dvpos.le, abs_of_nonneg (by rw [sub_nonneg]; exact dvg1.le),    ENNReal.ofNNReal_toNNReal, ENNReal.ofReal_rpow_of_pos dvpos, ← ENNReal.ofReal_mul zero_le_two,    ENNReal.ofReal_rpow_of_pos (by rwa [inv_pos, sub_pos]),    ← ENNReal.ofReal_mul' (Real.rpow_nonneg ipos.le _)]  have Acast : ENNReal.ofNNReal (defaultA a ^ 2) = ENNReal.ofReal (2 ^ (a * 2)) := by    simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat, ENNReal.coe_pow, ENNReal.coe_ofNat]    norm_cast; rw [pow_mul]  rw [Acast, ENNReal.ofReal_rpow_of_pos (by positivity), ← ENNReal.ofReal_mul' (by positivity),    mul_assoc, ← Real.mul_rpow ipos.le (by positivity), ← ENNReal.toNNReal_rpow,    mul_assoc, ← Real.mul_rpow dvpos.le (by positivity), ENNReal.ofReal_rpow_of_pos (by positivity)]  have RHScast : (2 : ℝ≥0) ^ (a + 2) = (ENNReal.ofReal (2 ^ (a + 2))).toNNReal := by    rw [ENNReal.ofReal_pow zero_le_two, ENNReal.toNNReal_pow]; norm_cast  rw [RHScast]; refine ENNReal.toNNReal_mono (by finiteness) (ENNReal.ofReal_le_ofReal ?_)  -- Now everything is in `ℝ`  calc    _ = (2 * (2 / (2 - q₆ a) * 2 ^ (a * 2)) ^ (2 / q₆ a)⁻¹) ^ (q₆ a)⁻¹ := by      rw [← mul_assoc]; congr 4      rw [← div_eq_mul_inv, div_div, mul_sub_one, mul_div_cancel₀ _ (q₆_pos a4).ne']    _ ≤ (2 * (2 ^ ((1 + a) * 2)) ^ (2 / q₆ a)⁻¹) ^ (q₆ a)⁻¹ := by      have : 0 < 2 / (2 - q₆ a) := by        apply div_pos zero_lt_two; rw [sub_pos]        exact (q₆_le_superparticular a4).trans_lt (by norm_num)      rw [one_add_mul, pow_add]; gcongr      · rw [inv_nonneg]; exact (q₆_pos a4).le      · rw [sq, ← div_inv_eq_mul]; apply div_le_div_of_nonneg_left (by norm_num) (by norm_num)        rw [le_sub_comm]; exact (q₆_le_superparticular a4).trans (by norm_num)    _ = 2 ^ (q₆ a)⁻¹ * 2 ^ (1 + a) := by      rw [Real.mul_rpow zero_le_two (by positivity), ← Real.rpow_mul (by positivity), inv_div,        ← div_eq_mul_inv, div_div_cancel_left' (q₆_pos a4).ne', pow_mul, ← Real.rpow_natCast,        ← Real.rpow_mul (by positivity), show (2 : ℕ) * 2⁻¹ = (1 : ℝ) by norm_num, Real.rpow_one]    _ ≤ _ := by      rw [pow_succ', add_comm]; gcongr      apply Real.rpow_le_self_of_one_le one_le_two      rw [inv_le_one_iff₀]; exact Or.inr (one_lt_q₆ a4).le