rw [abs_of_nonneg (Int.fract_nonneg _)]
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
d : ℕ
⊢ |Int.fract (↑N / ↑d)| < 1
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
d : ℕ
⊢ Int.fract (↑N / ↑d) < 1