tendsto_tsum_of_monotone_convergence

lemma tendsto_tsum_of_monotone_convergence    {β : Type*} {f : ℕ → β → ENNReal} {g : β → ENNReal}    (hmono : ∀ k, Monotone (fun n => f n k))    (hlim : ∀ k, Tendsto (fun n => f n k) atTop (𝓝 (g k))) :    Tendsto (fun n => ∑' k, f n k) atTop (𝓝 (∑' k, g k)) := by  letI : MeasurableSpace β := ⊤  let μ : Measure β := Measure.count  have hg_iSup (k : β) : (⨆ n : ℕ, f n k) = g k := iSup_eq_of_tendsto (hmono k) (hlim k)  have h_tend_lint : Tendsto (fun n => ∫⁻ k, f n k ∂μ) atTop (𝓝 (∫⁻ k, (⨆ n, f n k) ∂μ)) := by    have hmeas : ∀ n, Measurable fun k : β => f n k := fun _ _ _ ↦ trivial    have hmono_fn : Monotone (fun n => fun k : β => f n k) := fun _ _ hnm k ↦ hmono k hnm    simpa [lintegral_iSup hmeas hmono_fn] using      tendsto_atTop_iSup fun _ _ hmn ↦ lintegral_mono fun k ↦ hmono k hmn  simpa [μ, lintegral_count, hg_iSup] using h_tend_lint