case h.e'_6
α : Type u_2
β : Type u_1
γ : Type ?u.41040
δ : Type ?u.41043
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ a = if b = b then a else 0
α : Type u_2
β : Type u_1
γ : Type ?u.41040
δ : Type ?u.41043
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ HasSum (fun b' => if b' = b then a else 0) a
convert @hasSum_single _ _ _ _ (fun b' => if b' = b then a else 0) b (fun b' hb' => if_neg hb')
no goals
case h.e'_6
α : Type u_2
β : Type u_1
γ : Type ?u.41040
δ : Type ?u.41043
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b✝ : α
s : Finset β
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ a = if b = b then a else 0
exact (if_pos rfl).symm