no goals
α : Type u_2
β : Type u_1
γ : Type ?u.304262
δ : Type ?u.304265
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s t : Set β
h : s = t
⊢ (∑' (x : ↑s), f ↑x) = ∑' (x : ↑t), f ↑x
rw [h]