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
d : ℕ
⊢ |if Squarefree d then (-1) ^ Ω d else 0| ≤ 1
no goals