Ramanujan.Calculations.C3_le_one_of

theorem C3_le_one_of    {xₐ : ℝ}    (hxₐ : xₐ = exp (3914 : ℝ))    (hlogxₐ : log xₐ = (3914 : ℝ)) :    2 * log xₐ ^ 6 / xₐ * ∑ k ∈ Finset.Icc 1 5, (k.factorial : ℝ) / log 2 ^ (k + 1)      ≤ (1 : ℝ) := by  rw [hlogxₐ, hxₐ]  simp only [Nat.reduceAdd, Nat.one_le_ofNat, Finset.sum_Icc_succ_top, Finset.Icc_self,    Finset.sum_singleton, Nat.factorial, Nat.succ_eq_add_one, zero_add, mul_one, Nat.cast_one,    one_div, Nat.cast_ofNat, Nat.reduceMul]  have hA : 2 * (3914 : ℝ) ^ 6 * exp (-(3914 : ℝ)) ≤ (1 : ℝ) / 1000000 := exp_3914_poly_small  let u : ℝ := (log 2)⁻¹  have hu_le : u ≤ (2 : ℝ) := by    dsimp [u]    have hhalf : (1 / 2 : ℝ) ≤ log 2 := by linarith [log_two_gt_d9]    have h := one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 1 / 2) hhalf    simpa [one_div] using h  have hB :      ((log 2 ^ 2)⁻¹ + 2 / log 2 ^ 3 + 6 / log 2 ^ 4 + 24 / log 2 ^ 5 + 120 / log 2 ^ 6) ≤ (9000 : ℝ) := by    rw [show ((log 2 ^ 2)⁻¹ + 2 / log 2 ^ 3 + 6 / log 2 ^ 4 + 24 / log 2 ^ 5 + 120 / log 2 ^ 6)        = u ^ 2 + 2 * u ^ 3 + 6 * u ^ 4 + 24 * u ^ 5 + 120 * u ^ 6 by dsimp [u]; ring_nf]    exact le_trans (show u ^ 2 + 2 * u ^ 3 + 6 * u ^ 4 + 24 * u ^ 5 + 120 * u ^ 6        ≤ 2 ^ 2 + 2 * 2 ^ 3 + 6 * 2 ^ 4 + 24 * 2 ^ 5 + 120 * 2 ^ 6 by gcongr) (by norm_num)  rw [show 2 * (3914 : ℝ) ^ 6 / exp (3914 : ℝ)      = 2 * (3914 : ℝ) ^ 6 * exp (-(3914 : ℝ)) by    field_simp; rw [show (1 : ℝ) = exp (3914 : ℝ) * exp (-(3914 : ℝ)) by rw [← exp_add]; norm_num]]  exact le_trans (mul_le_mul hA hB (by positivity) (by positivity)) (by norm_num)