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

State before:
s : Sieve
⊢ s.siftedSum = ∑ d ∈ A, s.weights d * δ (P.gcd d)
Tactic:
dsimp only [siftedSum]
State after:
s : Sieve
⊢ (∑ d ∈ A, if P.Coprime d then s.weights d else 0) = ∑ d ∈ A, s.weights d * δ (P.gcd d)

State before:
s : Sieve
⊢ (∑ d ∈ A, if P.Coprime d then s.weights d else 0) = ∑ d ∈ A, s.weights d * δ (P.gcd d)
Tactic:
apply sum_congr rfl
State after:
s : Sieve
⊢ ∀ x ∈ A, (if P.Coprime x then s.weights x else 0) = s.weights x * δ (P.gcd x)

State before:
s : Sieve
⊢ ∀ x ∈ A, (if P.Coprime x then s.weights x else 0) = s.weights x * δ (P.gcd x)
Tactic:
intro d _
State after:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.Coprime d then s.weights d else 0) = s.weights d * δ (P.gcd d)

State before:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.Coprime d then s.weights d else 0) = s.weights d * δ (P.gcd d)
Tactic:
dsimp only [Nat.Coprime, delta] at *
State after:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = s.weights d * if P.gcd d = 1 then 1 else 0

State before:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = s.weights d * if P.gcd d = 1 then 1 else 0
Tactic:
rw [mul_ite_zero]
State after:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = if P.gcd d = 1 then s.weights d * 1 else 0

State before:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = if P.gcd d = 1 then s.weights d * 1 else 0
Tactic:
exact if_congr Iff.rfl (symm $ mul_one _) rfl
State after:
no goals