Theorem: Sieve.selbergTerms_apply (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
d : ℕ
⊢ g d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
unfold selbergTerms
State after:
s : Sieve
d : ℕ
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)

State before:
s : Sieve
d : ℕ
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
by_cases h : d=0
State after:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)

case neg
s : Sieve
d : ℕ
h : ¬d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)

State before:
case neg
s : Sieve
d : ℕ
h : ¬d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
rw [ArithmeticFunction.pmul_apply, ArithmeticFunction.prodPrimeFactors_apply h]
State after:
no goals

State before:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
Tactic:
rw [h]
State after:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) 0 = ν 0 * ∏ p ∈ primeFactors 0, 1 / (1 - ν p)

State before:
case pos
s : Sieve
d : ℕ
h : d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) 0 = ν 0 * ∏ p ∈ primeFactors 0, 1 / (1 - ν p)
Tactic:
simp
State after:
no goals