rw [←moebius_inv_dvd_lower_bound _ _ (Squarefree.squarefree_of_dvd hm hP),
  sum_over_dvd_ite hP.ne_zero hm]
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then μ d else 0) = if l = m then μ l else 0
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