WeakPNT''

theorem WeakPNT'' : ψ ~[atTop] (fun x ↦ x) := by    rw [(by rfl : ψ = (fun x ↦ ψ x))]    simp_rw [Chebyshev.psi_eq_sum_Icc]    apply IsEquivalent.trans (v := fun x ↦ (⌊x⌋₊:ℝ))    · rw [isEquivalent_iff_tendsto_one]      · convert! Tendsto.comp WeakPNT' tendsto_nat_floor_atTop        infer_instance      rw [eventually_iff]      simp only [ne_eq, cast_eq_zero, floor_eq_zero, not_lt, mem_atTop_sets,        Set.mem_setOf_eq]      use 1      simp only [imp_self, implies_true]    apply IsLittleO.isEquivalent    rw [← isLittleO_neg_left]    apply IsLittleO.of_bound    intro ε hε    simp only [Pi.sub_apply, neg_sub, norm_eq_abs, eventually_atTop]    use ε⁻¹    intro b hb    have hb' : 0 ≤ b := le_of_lt (lt_of_lt_of_le (inv_pos_of_pos hε) hb)    rw [abs_of_nonneg, abs_of_nonneg hb']    · apply LE.le.trans _ ((inv_le_iff_one_le_mul₀' hε).mp hb)      linarith [Nat.lt_floor_add_one b]    rw [sub_nonneg]    exact floor_le hb'