norm_cast
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |↑(μ d)| ≤ 1
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |μ d| ≤ 1