rw [abs_le, neg_sub] at h_bound
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
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound :
  1 - ↑N ≤ ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ∧
    ∑ 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
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1