Theorem: tsum_subtype_eq_tsum_subtype (Matroid/ForMathlib/ENatTopology.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s t : Set α
h : s ∩ support f = t ∩ support f
⊢ ∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x
Tactic:
rw [← tsum_inter_support_eq_tsum_subtype, eq_comm, ← tsum_inter_support_eq_tsum_subtype, h]
State after:
no goals