α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
h : HasSum (fun b_1 => f b_1 + if b_1 = b then x else 0) (a + x)
⊢ a + x = a' + f b
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
⊢ a + x = a' + f b
have h := hf.add (hasSum_ite_eq b x)
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
h : HasSum (fun b_1 => update f b x b_1 + if b_1 = b then f b else 0) (a + x)
⊢ a + x = a' + f b
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
h : HasSum (fun b_1 => f b_1 + if b_1 = b then x else 0) (a + x)
⊢ a + x = a' + f b
simp_rw [this] at h
no goals
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
this : ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
h : HasSum (fun b_1 => update f b x b_1 + if b_1 = b then f b else 0) (a + x)
⊢ a + x = a' + f b
exact HasSum.unique h (hf'.add (hasSum_ite_eq b (f b)))
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
⊢ (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
⊢ ∀ (b' : β), (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
intro b'
case inl
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
hb' : b' = b
⊢ f b' + x = update f b x b' + f b

case inr
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
hb' : ¬b' = b
⊢ f b' + 0 = update f b x b' + 0
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
⊢ (f b' + if b' = b then x else 0) = update f b x b' + if b' = b then f b else 0
split_ifs with hb'
no goals
case inl
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
hb' : b' = b
⊢ f b' + x = update f b x b' + f b
simpa only [Function.update_apply, hb', eq_self_iff_true] using add_comm (f b) x
no goals
case inr
α✝ : Type ?u.283335
β✝ : Type ?u.283338
γ : Type ?u.283341
δ : Type ?u.283344
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 a' : α
hf : HasSum f a
b : β
x : α
hf' : HasSum (update f b x) a'
b' : β
hb' : ¬b' = b
⊢ f b' + 0 = update f b x b' + 0
simp only [Function.update_apply, hb', if_false]