log_nth_prime_asymp

lemma log_nth_prime_asymp : (fun n ↦ log (nth_prime n)) ~[atTop] (fun n ↦ log n) := by  have := pi_nth_prime_asymp.log tendsto_natCast_atTop_atTop  · apply IsEquivalent.trans _ this    apply IsEquivalent.congr_right (v := (fun n ↦ log (nth_prime n) - log (log (nth_prime n))))    swap    · filter_upwards with n      rw [log_div]      · exact_mod_cast prime_nth_prime n |>.ne_zero      · apply log_ne_zero.mpr ⟨?_, ?_, ?_⟩        <;> norm_cast<;> linarith [prime_nth_prime n |>.two_le]    symm    apply IsEquivalent.sub_isLittleO (by rfl)    apply IsLittleO.comp_tendsto isLittleO_log_id_atTop    have : Tendsto (fun n ↦ ((nth_prime n) : ℝ)) atTop atTop := by      apply tendsto_natCast_atTop_iff.mpr tendsto_nth_prime_atTop    apply tendsto_log_atTop.comp this