cauchySeq_intervalIntegral_real_sinc_atTop

theorem cauchySeq_intervalIntegral_real_sinc_atTop :    CauchySeq (fun A : ℝ => ∫ x in (0 : ℝ)..A, Real.sinc x) := by  refine Metric.cauchySeq_iff.2 ?_  intro ε hε  have hlim : Filter.Tendsto (fun M : ℝ => 3 * M⁻¹) Filter.atTop (nhds 0) := by    simpa using (tendsto_const_nhds.mul tendsto_inv_atTop_zero : Filter.Tendsto      (fun M : ℝ => 3 * M⁻¹) Filter.atTop (nhds (3 * 0)))  have hsmall : ∀ᶠ M : ℝ in Filter.atTop, 3 * M⁻¹ < ε :=    hlim.eventually (gt_mem_nhds hε)  have hlarge : ∀ᶠ M : ℝ in Filter.atTop, 1 ≤ M := Filter.eventually_ge_atTop 1  rcases Filter.eventually_atTop.1 (hsmall.and hlarge) with ⟨M, hM⟩  refine ⟨M, ?_⟩  intro A hA B hB  have hMsmall : 3 * M⁻¹ < ε := (hM M le_rfl).1  have hM_one : 1 ≤ M := (hM M le_rfl).2  have hM_pos : 0 < M := zero_lt_one.trans_le hM_one  have hA_one : 1 ≤ A := hM_one.trans hA  have hB_one : 1 ≤ B := hM_one.trans hB  by_cases hAB : A ≤ B  · have hsub :        (∫ x in (0 : ℝ)..B, Real.sinc x) -          (∫ x in (0 : ℝ)..A, Real.sinc x) =            ∫ x in A..B, Real.sinc x := by      exact intervalIntegral.integral_interval_sub_left        (Real.continuous_sinc.intervalIntegrable _ _)        (Real.continuous_sinc.intervalIntegrable _ _)    have hinv : A⁻¹ ≤ M⁻¹ := by      simpa [one_div] using one_div_le_one_div_of_le hM_pos hA    calc      dist (∫ x in (0 : ℝ)..A, Real.sinc x) (∫ x in (0 : ℝ)..B, Real.sinc x)          = dist (∫ x in (0 : ℝ)..B, Real.sinc x) (∫ x in (0 : ℝ)..A, Real.sinc x) :=            dist_comm _ _      _ = ‖(∫ x in (0 : ℝ)..B, Real.sinc x) -            (∫ x in (0 : ℝ)..A, Real.sinc x)‖ := by            rw [Real.dist_eq, Real.norm_eq_abs]      _ = ‖∫ x in A..B, Real.sinc x‖ := by rw [hsub]      _ ≤ 3 * A⁻¹ := norm_intervalIntegral_sinc_tail_le hA_one hAB      _ ≤ 3 * M⁻¹ := mul_le_mul_of_nonneg_left hinv (by norm_num)      _ < ε := hMsmall  · have hBA : B ≤ A := le_of_not_ge hAB    have hsub :        (∫ x in (0 : ℝ)..A, Real.sinc x) -          (∫ x in (0 : ℝ)..B, Real.sinc x) =            ∫ x in B..A, Real.sinc x := by      exact intervalIntegral.integral_interval_sub_left        (Real.continuous_sinc.intervalIntegrable _ _)        (Real.continuous_sinc.intervalIntegrable _ _)    have hinv : B⁻¹ ≤ M⁻¹ := by      simpa [one_div] using one_div_le_one_div_of_le hM_pos hB    calc      dist (∫ x in (0 : ℝ)..A, Real.sinc x) (∫ x in (0 : ℝ)..B, Real.sinc x)          = ‖(∫ x in (0 : ℝ)..A, Real.sinc x) -            (∫ x in (0 : ℝ)..B, Real.sinc x)‖ := by            rw [Real.dist_eq, Real.norm_eq_abs]      _ = ‖∫ x in B..A, Real.sinc x‖ := by rw [hsub]      _ ≤ 3 * B⁻¹ := norm_intervalIntegral_sinc_tail_le hB_one hBA      _ ≤ 3 * M⁻¹ := mul_le_mul_of_nonneg_left hinv (by norm_num)      _ < ε := hMsmall