no goals
α : Type u_1
β : Type u_2
γ : Type ?u.275475
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g✝ : α → ℝ≥0∞
f : α → β
hf : Surjective f
g : β → ℝ≥0∞
⊢ (∑' (y : β), g y) = ∑' (y : β), g (f (surjInv hf y))
simp only [surjInv_eq hf]