-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem limsup_measure_closed_le_iff_liminf_measure_open_ge {ι : Type*} {L : Filter ι}
    {μ : Measure Ω} {μs : ι → Measure Ω} [IsProbabilityMeasure μ]
    [∀ i, IsProbabilityMeasure (μs i)] :
    (∀ F, IsClosed F → (L.limsup fun i ↦ μs i F) ≤ μ F) ↔
      ∀ G, IsOpen G → μ G ≤ L.liminf fun i ↦ μs i G

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F) ↔
    ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L

Tactic:
constructor

Result:
case mp
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F) →
    ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L

case mpr
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L) →
    ∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F

Proof state:
case mpr
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L
F : Set Ω
F_closed : IsClosed F
⊢ limsup (fun i => (μs i) F) L ≤ μ F

Tactic:
exact limsup_measure_le_of_le_liminf_measure_compl
  F_closed.measurableSet (h Fᶜ (isOpen_compl_iff.mpr F_closed))

Result:
no goals

Proof state:
case mp
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F) →
    ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L

Tactic:
intro h G G_open

Result:
case mp
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F
G : Set Ω
G_open : IsOpen G
⊢ μ G ≤ liminf (fun i => (μs i) G) L

Proof state:
case mp
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F
G : Set Ω
G_open : IsOpen G
⊢ μ G ≤ liminf (fun i => (μs i) G) L

Tactic:
exact le_measure_liminf_of_limsup_measure_compl_le
  G_open.measurableSet (h Gᶜ (isClosed_compl_iff.mpr G_open))

Result:
no goals

Proof state:
case mpr
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L) →
    ∀ (F : Set Ω), IsClosed F → limsup (fun i => (μs i) F) L ≤ μ F

Tactic:
intro h F F_closed

Result:
case mpr
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) L
F : Set Ω
F_closed : IsClosed F
⊢ limsup (fun i => (μs i) F) L ≤ μ F