FKS2.tendsto_log_div_self_mul_integral_atTop_zero

lemma tendsto_log_div_self_mul_integral_atTop_zero {x₁ : ℝ} (hx₁ : 14 ≤ x₁) :    Filter.Tendsto (fun y ↦ (Real.log y / y) * ∫ s in x₁..y, 1 / (Real.log s) ^ 2) Filter.atTop (nhds 0) := by  have h_lim : Filter.Tendsto (fun y ↦ Real.log x₁ / (Real.log x₁ - 2) / Real.log y) Filter.atTop (nhds 0) := by    have h_inv : Filter.Tendsto (fun y ↦ (Real.log y)⁻¹) Filter.atTop (nhds 0) :=      Filter.Tendsto.comp tendsto_inv_atTop_zero Real.tendsto_log_atTop    have := tendsto_const_nhds (x := Real.log x₁ / (Real.log x₁ - 2)) |>.mul h_inv    simp only [mul_zero] at this    rwa [show (fun x ↦ Real.log x₁ / (Real.log x₁ - 2) * (Real.log x)⁻¹) =        (fun y ↦ Real.log x₁ / (Real.log x₁ - 2) / Real.log y) by ext y; ring] at this  refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h_lim ?_ ?_  · filter_upwards [Filter.eventually_ge_atTop x₁] with y hy    exact log_div_self_mul_integral_nonneg hx₁ hy  · filter_upwards [Filter.eventually_ge_atTop x₁] with y hy    exact log_div_self_mul_integral_le_of_ge hx₁ hy