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

State before:
s : Sieve
d : ℕ
⊢ s.multSum d = ν d * X + s.rem d
Tactic:
dsimp [rem]
State after:
s : Sieve
d : ℕ
⊢ (∑ n ∈ A, if d ∣ n then s.weights n else 0) = ν d * X + ((∑ n ∈ A, if d ∣ n then s.weights n else 0) - ν d * X)

State before:
s : Sieve
d : ℕ
⊢ (∑ n ∈ A, if d ∣ n then s.weights n else 0) = ν d * X + ((∑ n ∈ A, if d ∣ n then s.weights n else 0) - ν d * X)
Tactic:
ring
State after:
no goals