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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g✝ : α → ℕ∞
f : α → β
hf : Surjective f
g : β → ℕ∞
⊢ ∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))
Tactic:
simp only [surjInv_eq hf]
State after:
no goals