have hf' (d : ℕ) : |Int.fract ((N : ℚ) / d)| < 1 := by
  rw [abs_of_nonneg (Int.fract_nonneg _)]
  exact Int.fract_lt_one _
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⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1