-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
lemma lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
    {μ : Measure Ω} {μs : ℕ → Measure Ω} {f : Ω → ℝ} (f_cont : Continuous f) (f_nn : 0 ≤ f)
    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
    ∫⁻ x, ENNReal.ofReal (f x) ∂μ ≤ atTop.liminf (fun i ↦ ∫⁻ x, ENNReal.ofReal (f x) ∂ (μs i))

Proof state:
case calc_1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i => (μs i) {a | t < f a}) atTop

Tactic:
exact (lintegral_mono (fun t ↦ h_opens _ (continuous_def.mp f_cont _ isOpen_Ioi))).trans
        (le_refl _)

Result:
no goals

Proof state:
case calc_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i => (μs i) {a | t < f a}) atTop ≤
    liminf (fun i => ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop

Tactic:
exact lintegral_liminf_le (fun n ↦ Antitone.measurable (fun s t hst ↦
        measure_mono (fun ω hω ↦ lt_of_le_of_lt hst hω)))

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop

Tactic:
simp_rw [lintegral_eq_lintegral_meas_lt _ (Eventually.of_forall f_nn) f_cont.aemeasurable]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ liminf (fun i => ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ liminf (fun i => ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop

Tactic:
calc  ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
    ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, atTop.liminf (fun i ↦ (μs i) {a | t < f a}) := ?_ _ ≤ atTop.liminf (fun i ↦ ∫⁻ (t : ℝ) in Set.Ioi 0, (μs i) {a | t < f a}) := ?_

Result:
case calc_1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i => (μs i) {a | t < f a}) atTop

case calc_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, liminf (fun i => (μs i) {a | t < f a}) atTop ≤
    liminf (fun i => ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop