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