Theorem: Aux.moebius_inv_dvd_lower_bound' (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
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
Tactic:
rw [←moebius_inv_dvd_lower_bound _ _ (Squarefree.squarefree_of_dvd hm hP),
  sum_over_dvd_ite hP.ne_zero hm]
State after:
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

State before:
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
Tactic:
simp_rw[ite_and, ←sum_filter, filter_comm]
State after:
no goals