rw [eq_sub_iff_add_eq, eq_comm, ← eq_div_iff (by norm_num [Nat.pos_iff_ne_zero.mp hN])] at h_sum
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N - ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1