intro d _ hdl
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
d : ℕ
a✝ : d ∈ m.divisors
hdl : d ≠ l
⊢ (μ (m / d) • if l = d then μ l else 0) = 0