case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
x✝ : β
⊢ Function.update f b a x✝ = (if x✝ = b then a - f b else 0) + f x✝
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
⊢ HasSum (Function.update f b a) (a - f b + a₁)
convert (hasSum_ite_eq b (a - f b)).add hf
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
x✝ : β
⊢ Function.update f b a x✝ = (if x✝ = b then a - f b else 0) + f x✝
rename_i b'
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
by_cases h : b' = b
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
. simp only [h, update_noteq, if_false, Ne.def, zero_add, not_false_iff]
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a - f b else 0) + f b
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
rw [h, update_same]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a - f b else 0) + f b
simp [eq_self_iff_true, if_true, sub_add_cancel]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.408116
δ : Type ?u.408119
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a✝ a₁ a₂ : α
hf : HasSum f a₁
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update f b a b' = (if b' = b then a - f b else 0) + f b'
simp only [h, update_noteq, if_false, Ne.def, zero_add, not_false_iff]