rw [sum_congr rfl (fun _ ↦ this), sum_const, smul_zero, add_zero, Int.cast_one]
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)
no goals