simp only [Int.fract, sub_sub_self]
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
d : ℕ
x✝ : d ∈ range (N + 1)
⊢ ↑(μ d) * ↑⌊↑N / ↑d⌋ = (fun d => ↑(μ d) * (↑N / ↑d - Int.fract (↑N / ↑d))) d
no goals