simp_rw[ite_and, ←sum_filter, filter_comm]
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then μ d else 0) = ∑ d ∈ P.divisors, if d ∣ m then if l ∣ d then μ d else 0 else 0
no goals