simp_rw [← coe_mul_zeta_apply, ArithmeticFunction.sum_Icc_mul_zeta, nsmul_eq_mul, mul_comm]
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ m ∈ Icc 1 N, ∑ d ∈ m.divisors, μ d) = ↑(∑ d ∈ range (N + 1), μ d * (↑N / ↑d))
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ range (N + 1), ↑N / ↑x * μ x)