all_goals simp [sum_ite, cast_sub hN]
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
⊢ ∑ i ∈ Ico 1 N, 1 ≤ ↑N - 1
no goals