no goals
α : Type u_2
β : Type u_1
γ : Type ?u.426874
δ : Type ?u.426877
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
⊢ HasSum f (a₁ + (a₂ - a₁)) ↔ HasSum f a₂
rw [add_sub_cancel'_right]