α✝ : Type ?u.290302
β✝ : Type ?u.290305
γ : Type ?u.290308
δ : Type ?u.290311
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
⊢ HasSum (update f b 0) a'
α✝ : Type ?u.290302
β✝ : Type ?u.290305
γ : Type ?u.290308
δ : Type ?u.290311
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
⊢ a = a' + f b
refine' (add_zero a).symm.trans (hf.update' b 0 _)
case h.e'_5.h
α✝ : Type ?u.290302
β✝ : Type ?u.290305
γ : Type ?u.290308
δ : Type ?u.290311
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
x✝ : β
⊢ update f b 0 x✝ = if x✝ = b then 0 else f x✝
α✝ : Type ?u.290302
β✝ : Type ?u.290305
γ : Type ?u.290308
δ : Type ?u.290311
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
⊢ HasSum (update f b 0) a'
convert hf'
no goals
case h.e'_5.h
α✝ : Type ?u.290302
β✝ : Type ?u.290305
γ : Type ?u.290308
δ : Type ?u.290311
inst✝⁶ : AddCommMonoid α✝
inst✝⁵ : TopologicalSpace α✝
f✝ g : β✝ → α✝
a✝ b✝ : α✝
s : Finset β✝
inst✝⁴ : ContinuousAdd α✝
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : AddCommMonoid α
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
f : β → α
a : α
hf : HasSum f a
b : β
a' : α
hf' : HasSum (fun n => if n = b then 0 else f n) a'
x✝ : β
⊢ update f b 0 x✝ = if x✝ = b then 0 else f x✝
apply update_apply