have h_bound : |∑ d in range (N + 1), μ d * Int.fract ((N : ℚ) / d)| ≤ N - 1 := by
  
  rw [range_eq_Ico, ← Ico_insert_succ_left, sum_insert, ArithmeticFunction.map_zero,
    Int.cast_zero, zero_mul, zero_add, Ico_succ_right]
  all_goals simp
  
  rw [← Ico_insert_right, sum_insert, div_self, Int.fract_one, mul_zero]
  all_goals simp [hN, Nat.pos_iff_ne_zero.mp hN]
  
  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]
  apply (abs_sum_le_sum_abs _ _).trans
  apply (sum_le_sum fun d _ ↦ this d).trans
  all_goals simp [sum_ite, cast_sub hN]
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
case pos
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
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1