rw [show (N : ℚ) = ((N : ℤ) : ℚ) by norm_cast, Rat.floor_int_div_nat_eq_div]
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑⌊↑N / ↑x✝⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑(↑N / ↑x✝)

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1