no goals
α : Type u_1
β : Type ?u.317051
γ : Type ?u.317054
δ : Type ?u.317057
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
f : Bool → α
⊢ (∑' (i : Bool), f i) = f (decide False) + f (decide True)
rw [tsum_fintype, Finset.sum_eq_add] <;> simp