have {x : ℕ} (hx : x ∈ Ioc 1 N) : ∑ d in divisors x, μ d = 0 := by
  rw [mem_Ioc] at hx
  simp only [← this, one_apply, hx.left.ne.symm, if_false]
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)
N : ℕ
hN : 1 ≤ N
this✝ : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
this : ∀ {x : ℕ}, x ∈ Ioc 1 N → ∑ d ∈ x.divisors, μ d = 0
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)