Theorem: SelbergSieve.selbergμPlus_eq_zero (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ≤ y
⊢ s.selbergMuPlus d = 0
Tactic:
apply Sieve.lambdaSquared_eq_zero_of_support _ y _ d hd
State after:
s : SelbergSieve
d : ℕ
hd : ¬↑d ≤ y
⊢ ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → s.selbergWeights d = 0

State before:
s : SelbergSieve
d : ℕ
hd : ¬↑d ≤ y
⊢ ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → s.selbergWeights d = 0
Tactic:
apply s.selbergWeights_eq_zero
State after:
no goals