α : Type u_1
β : Type u_2
γ : Type ?u.770476
δ : Type ?u.770479
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ (∑ x in s, f x + ∑' (x : { x // ¬x ∈ s }), f ↑x) = (∑' (x : ↑↑s), f ↑x) + ∑' (x : ↑(↑sᶜ)), f ↑x
α : Type u_1
β : Type u_2
γ : Type ?u.770476
δ : Type ?u.770479
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ (∑ x in s, f x + ∑' (x : { x // ¬x ∈ s }), f ↑x) = ∑' (x : β), f x
rw [← tsum_subtype_add_tsum_subtype_compl hf s]
α : Type u_1
β : Type u_2
γ : Type ?u.770476
δ : Type ?u.770479
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ (∑' (x : { x // ¬x ∈ s }), f ↑x) = ∑' (x : ↑(↑sᶜ)), f ↑x
α : Type u_1
β : Type u_2
γ : Type ?u.770476
δ : Type ?u.770479
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ (∑ x in s, f x + ∑' (x : { x // ¬x ∈ s }), f ↑x) = (∑' (x : ↑↑s), f ↑x) + ∑' (x : ↑(↑sᶜ)), f ↑x
simp only [Finset.tsum_subtype', add_right_inj]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.770476
δ : Type ?u.770479
inst✝⁴ : AddCommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformAddGroup α
f✝ g : β → α
a a₁ a₂ : α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Summable f
s : Finset β
⊢ (∑' (x : { x // ¬x ∈ s }), f ↑x) = ∑' (x : ↑(↑sᶜ)), f ↑x
rfl