-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
lemma integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure
    {μ : Measure Ω} {μs : ℕ → Measure Ω} [∀ i, IsProbabilityMeasure (μs i)]
    {f : Ω →ᵇ ℝ} (f_nn : 0 ≤ f)
    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
    ∫ x, (f x) ∂μ ≤ atTop.liminf (fun i ↦ ∫ x, (f x) ∂ (μs i))

Proof state:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
⊢ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop < ⊤

Tactic:
apply lt_of_le_of_lt _ (show (‖f‖₊ : ℝ≥0∞) < ∞ from ENNReal.coe_lt_top)

Result:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
⊢ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop ≤ ↑‖f‖₊

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

Tactic:
convert ENNReal.toReal_mono ?_ same

Result:
case h.e'_4
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
⊢ liminf (fun i => ∫ (x : Ω), f x ∂μs i) atTop = (liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop).toReal

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

Proof state:
case h.e'_3.h.e'_4.h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x✝ : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((fun f => f.toFun) f x) = ↑⟨(fun f => f.toFun) f x, ⋯⟩
⊢ ENNReal.ofReal (f x) = ↑‖f x‖₊

Tactic:
simp only [ContinuousMap.toFun_eq_coe, BoundedContinuousFunction.coe_toContinuousMap] at aux

Result:
case h.e'_3.h.e'_4.h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x✝ : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
x : Ω
aux : ENNReal.ofReal (f x) = ↑⟨f x, ⋯⟩
⊢ ENNReal.ofReal (f x) = ↑‖f x‖₊

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

Tactic:
rw [@integral_eq_lintegral_of_nonneg_ae Ω _ μ f (Eventually.of_forall f_nn)
      f.continuous.measurable.aestronglyMeasurable]

Result:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (f a) ∂μ).toReal ≤ liminf (fun i => ∫ (x : Ω), f x ∂μs i) atTop

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

Tactic:
have same := lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
                f.continuous f_nn h_opens

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

Proof state:
case h.e'_3.h.e'_4.h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x✝ : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
x : Ω
aux : ENNReal.ofReal (f x) = ↑⟨f x, ⋯⟩
⊢ ↑⟨f x, ⋯⟩ = ↑‖f x‖₊

Tactic:
congr

Result:
case h.e'_3.h.e'_4.h.e_a.e_val
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x✝ : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
x : Ω
aux : ENNReal.ofReal (f x) = ↑⟨f x, ⋯⟩
⊢ f x = ‖f x‖