apply (abs_sum_le_sum_abs _ _).trans
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ ∑ i ∈ Ico 1 N, |↑(μ i) * Int.fract (↑N / ↑i)| ≤ ↑N - 1