norm_num [Int.cast_sum]
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ d ∈ range (N + 1), μ d * (↑N / ↑d)) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
N : ℕ
hN : 1 ≤ N
⊢ ∑ x ∈ range (N + 1), ↑(μ x) * ↑(↑N / ↑x) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)