Theorem: Aux.ite_sum_zero (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
p : Prop
inst✝ : Decidable p
s : Finset ℕ
f : ℕ → ℝ
⊢ (if p then ∑ x ∈ s, f x else 0) = ∑ x ∈ s, if p then f x else 0
Tactic:
split_ifs <;> simp
State after:
no goals