Theorem: ENat.tsum_comp_eq_tsum_of_equiv (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g✝ : α → ℕ∞
e : α ≃ β
g : β → ℕ∞
⊢ ∑' (x : α), g (e x) = ∑' (y : β), g y
Tactic:
rw [ENat.tsum_comp_eq_tsum_of_bijective e.bijective]
State after:
no goals