intro d hd
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ ∀ x ∈ m.divisors, (μ (m / x) • if l = x then μ l else 0) = 0
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ (μ (m / d) • if l = d then μ l else 0) = 0