Theorem: Aux.moebius_inv_dvd_lower_bound_real (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:
norm_cast
State after:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ m then μ x else 0) = if l = m then μ l else 0

State before:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ m then μ x else 0) = if l = m then μ l else 0
Tactic:
apply moebius_inv_dvd_lower_bound' hP l m hm
State after:
no goals