no goals
α : Type ?u.272740
β : Type ?u.272743
γ : Type ?u.272746
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g✝ : α → ℝ≥0∞
f g : ℕ → ℝ≥0∞
h₁ : (∑' (i : ℕ), g i) ≠ ⊤
h₂ : g ≤ f
this : ∀ (i : ℕ), f i - g i + g i = f i
⊢ ((∑' (i : ℕ), f i - g i) + ∑' (i : ℕ), g i) = ∑' (i : ℕ), f i
simp only [← ENNReal.tsum_add, this]