Antichain.le_C6_1_6

lemma le_C6_1_6 (a4 : 4 ≤ a) :    (2 : ℝ≥0∞) ^ ((𝕔 + 1) * a ^ 3 / p₆ a) * ∑ n ∈ Finset.range N, (2 ^ (-(p₆ a)⁻¹)) ^ n ≤      C6_1_6 a := by  have p₆p := p₆_pos a4  calc    _ ≤ (2 : ℝ≥0∞) ^ ((𝕔 + 1) * a ^ 3 / p₆ a) * (8 * a ^ 4) := by      gcongr      calc        _ ≤ _ := ENNReal.sum_le_tsum _        _ = _ := ENNReal.tsum_geometric _        _ ≤ 2 * (ENNReal.ofReal (p₆ a)⁻¹)⁻¹ :=          near_1_geometric_bound ⟨by grw [inv_nonneg, p₆p.le],            by grw [inv_le_one₀ p₆p, (one_lt_p₆ a4).le]⟩        _ = _ := by rw [ENNReal.ofReal_inv_of_pos p₆p, inv_inv, p₆]; norm_cast; ring    _ ≤ 2 ^ (7 : ℝ) * 2 ^ (2 * a + 3) := by      gcongr      · exact one_le_two      · rw [div_le_iff₀ p₆p, p₆]; norm_cast; rw [show 7 * (4 * a ^ 4) = 28 * a * a ^ 3 by ring]        gcongr        linarith [c_le_100]      · exact_mod_cast calculation_6_1_6 a4    _ ≤ _ := by      rw [C6_1_6]; norm_cast; rw [← pow_add]; gcongr      · exact one_le_two      · lia