have (d : ℕ) : |μ d * Int.fract ((N : ℚ) / d)| ≤ 1 := by
  rw [abs_mul, ← one_mul 1]
  apply mul_le_mul ?_ (hf' _).le (abs_nonneg _) zero_le_one
  norm_cast
  simp [moebius]
  split_ifs <;> simp only [abs_zero, zero_le_one, abs_pow, abs_neg, abs_one, one_pow, le_refl]
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1