no goals
α : Type u_1
β : Type ?u.993590
γ : Type ?u.993593
δ : Type ?u.993596
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n)
⊢ (∫⁻ (a : α), liminf (fun n => f n a) atTop ∂μ) = ∫⁻ (a : α), ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i a ∂μ
simp only [liminf_eq_iSup_iInf_of_nat]