swap
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)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1