no goals
α : Type u_1
β : Type u_2
γ : Type ?u.326054
δ : Type ?u.326057
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f g : β → α
a a₁ a₂ : α
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
⊢ (∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
by_cases hP : P <;> simp [hP]