-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma tendsto_integral_of_forall_integral_le_liminf_integral {ι : Type*} {L : Filter ι}
    {μ : Measure X} [IsProbabilityMeasure μ] {μs : ι → Measure X} [∀ i, IsProbabilityMeasure (μs i)]
    (h : ∀ f : X →ᵇ ℝ, 0 ≤ f → ∫ x, f x ∂μ ≤ L.liminf (fun i ↦ ∫ x, f x ∂ (μs i)))
    (f : X →ᵇ ℝ) :
    Tendsto (fun i ↦ ∫ x, f x ∂ (μs i)) L (𝓝 (∫ x, f x ∂μ))

Proof state:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
have obs := BoundedContinuousFunction.isBounded_range_integral μs f

Result:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
⊢ Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Proof state:
case inr.h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i) _auto✝

Tactic:
exact bdd_above

Result:
no goals

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
⊢ BddAbove (?m.51032 '' Set.univ)

Tactic:
simpa using obs.bddAbove

Result:
no goals

Proof state:
case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
key : ∫ (x : X), f x ∂μ + ‖f‖ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i + ‖f‖) L
this : liminf (fun i => (fun i => ∫ (x : X), f x ∂μs i) i + ‖f‖) L = liminf (fun i => ∫ (x : X), f x ∂μs i) L + ‖f‖
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L

Tactic:
rwa [this, add_le_add_iff_right] at key

Result:
no goals

Proof state:
case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L

Tactic:
have key := h _ (f.add_norm_nonneg)

Result:
case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
key : ∫ (x : X), (f + const X ‖f‖) x ∂μ ≤ liminf (fun i => ∫ (x : X), (f + const X ‖f‖) x ∂μs i) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L

Proof state:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)

Result:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Proof state:
case inr.hsup
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
have key := h _ (f.norm_sub_nonneg)

Result:
case inr.hsup
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
key : ∫ (x : X), (const X ‖f‖ - f) x ∂μ ≤ liminf (fun i => ∫ (x : X), (const X ‖f‖ - f) x ∂μs i) L
⊢ limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ