rw[mem_divisors] at h
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : l ∉ m.divisors
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ (μ (m / l) • if l = l then μ l else 0) = 0