case h.e'_5
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ (fun n => if n = b then 0 else f n) = update f b 0

case h.e'_6
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ a - f b = 0 - f b + a
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ HasSum (fun n => if n = b then 0 else f n) (a - f b)
convert hf.update b 0 using 1
case h.e'_5.h
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b n : β
⊢ (if n = b then 0 else f n) = update f b 0 n
case h.e'_5
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ (fun n => if n = b then 0 else f n) = update f b 0
ext n
no goals
case h.e'_5.h
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b n : β
⊢ (if n = b then 0 else f n) = update f b 0 n
rw [Function.update_apply]
no goals
case h.e'_6
α : Type u_2
β : Type u_1
γ : Type ?u.436486
δ : Type ?u.436489
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : DecidableEq β
hf : HasSum f a
b : β
⊢ a - f b = 0 - f b + a
rw [sub_add_eq_add_sub, zero_add]