-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type*} {L : Filter ι}
    [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω]
    [OpensMeasurableSpace Ω] {μ : FiniteMeasure Ω}
    {μs : ι → FiniteMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ)) {F : Set Ω} (F_closed : IsClosed F) :
    (L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F

Proof state:
case inr.h.intro
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2 ≤ ↑μ F + ↑ε

Tactic:
apply le_trans (add_le_add (hM M rfl.le).le (le_refl (ε / 2 : ℝ≥0∞)))

Result:
case inr.h.intro
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ ↑μ F + ↑ε / 2 + ↑ε / 2 ≤ ↑μ F + ↑ε

Proof state:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
⊢ ∀ (ε : ℝ≥0), 0 < ε → ↑μ F < ⊤ → limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Tactic:
intro ε ε_pos _

Result:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Proof state:
case inr.h.intro
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Tactic:
apply (Filter.limsup_le_limsup ev_near').trans

Result:
case inr.h.intro
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ limsup (fun x => ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2) L ≤ ↑μ F + ↑ε

Proof state:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Result:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
⊢ ∀ (ε : ℝ≥0), 0 < ε → ↑μ F < ⊤ → limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Proof state:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Tactic:
have ε_pos' := (ENNReal.half_pos (ENNReal.coe_ne_zero.mpr ε_pos.ne.symm)).ne.symm

Result:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε