x_log_x_atTop

lemma x_log_x_atTop : Filter.Tendsto (fun x => x / Real.log x) Filter.atTop Filter.atTop := by  have inv_log_x_div := Filter.Tendsto.comp (f := fun x => Real.log x / x) (g := fun x => x⁻¹)    (x := Filter.atTop) (y := (nhdsWithin 0 (Set.Ioi 0))) (z := Filter.atTop) ?_ ?_  · simp_rw [Function.comp_def, inv_div] at inv_log_x_div    exact inv_log_x_div  · exact tendsto_inv_nhdsGT_zero (𝕜 := ℝ)  · rw [tendsto_nhdsWithin_iff]    refine ⟨?_, ?_⟩    · have log_div_x := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 (by simp)      simp only [pow_one, one_mul, add_zero] at log_div_x      exact log_div_x    · simp only [Set.mem_Ioi, eventually_atTop]      use 2      intro x hx      have log_pos: 0 < Real.log x := by        refine (Real.log_pos_iff ?_).mpr ?_ <;> linarith      positivity