rw [if_pos hl, sum_eq_single l]
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m

case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ ∀ b ∈ m.divisors, b ≠ l → (μ (m / b) • if l = b then μ l else 0) = 0

case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ l ∉ m.divisors → (μ (m / l) • if l = l then μ l else 0) = 0