no goals
α : Type u_1
β : Type u_2
γ : Type ?u.347788
δ : Type ?u.347791
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
n : β
⊢ f n = (if n = b then f n else 0) + update f b 0 n
split_ifs with h <;> simp [update_apply, h]
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.347788
δ : Type ?u.347791
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ (∑' (x : β), if x = b then f x else 0) = if b = b then f b else 0
α : Type u_1
β : Type u_2
γ : Type ?u.347788
δ : Type ?u.347791
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ ((∑' (x : β), if x = b then f x else 0) + ∑' (x : β), update f b 0 x) =
    (if b = b then f b else 0) + ∑' (x : β), update f b 0 x
congr
no goals
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.347788
δ : Type ?u.347791
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ (∑' (x : β), if x = b then f x else 0) = if b = b then f b else 0
exact tsum_eq_single b fun b' hb' => if_neg hb'
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.347788
δ : Type ?u.347791
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
inst✝ : ContinuousAdd α
f : β → α
b : β
hf : Summable (update f b 0)
⊢ ((if b = b then f b else 0) + ∑' (x : β), update f b 0 x) = f b + ∑' (x : β), if x = b then 0 else f x
simp only [update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite]