awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
inl :
  ∀
    (h :
      LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) ⊥ : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
      (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) ⊥ : ℝ≥0∞)
inr :
  ∀ (hne : L.NeBot),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
      (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)

Tactic:
rcases L.eq_or_neBot with rfl | hne

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) ⊥ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) ⊥ : ℝ≥0∞)

Tactic:
simp only [liminf_bot, le_top]

Premises used: le_top, Filter.liminf_bot
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
⊢ (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_lt_top, MeasureTheory.IsProbabilityMeasure.measure_univ, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
⊢ (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
have meas_Ec : μ Eᶜ = 1 - μ E := by
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
i : ι
⊢ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_lt_top, MeasureTheory.IsProbabilityMeasure.measure_univ, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
⊢ ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
have meas_i_Ec : ∀ i, μs i Eᶜ = 1 - μs i E := by
    intro i
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
meas_i_Ec :
  ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
inr :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) ≤
    liminf (fun (i : ι) ↦ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)

Tactic:
simp_rw [meas_Ec, meas_i_Ec]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
meas_i_Ec :
  ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) 1 (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L) =
    liminf ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L

Tactic:
have key := antitone_const_tsub.map_limsup_of_continuousAt (F := L)
    (fun i ↦ μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
meas_i_Ec :
  ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
key :
  HSub.hSub (α := ℝ≥0∞) 1 (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L) =
    liminf ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) ≤
    liminf ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L

Tactic:
simpa [← key] using antitone_const_tsub h

Premises used: antitone_const_tsub
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)

Tactic:
compl_compl E ▸ le_measure_compl_liminf_of_limsup_measure_le (MeasurableSet.compl E_mble) h

Premises used: compl_compl, Eq.rec, MeasurableSet.compl, MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
inl :
  ∀
    (h :
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
        (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) ⊥ : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) ⊥ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
inr :
  ∀ (hne : L.NeBot),
    LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)

Tactic:
rcases L.eq_or_neBot with rfl | hne

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) ⊥ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) ⊥ : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)

Tactic:
simp only [limsup_bot, bot_le]

Premises used: Filter.limsup_bot, bot_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
⊢ (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_lt_top, MeasureTheory.IsProbabilityMeasure.measure_univ, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
⊢ (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
have meas_Ec : μ Eᶜ = 1 - μ E := by
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
i : ι
⊢ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_lt_top, MeasureTheory.IsProbabilityMeasure.measure_univ, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
⊢ ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
have meas_i_Ec : ∀ i, μs i Eᶜ = 1 - μs i E := by
    intro i
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
meas_i_Ec :
  ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
inr :
  limsup (fun (i : ι) ↦ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)

Tactic:
simp_rw [meas_Ec, meas_i_Ec]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
meas_i_Ec :
  ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) 1 (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L) =
    limsup ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L

Tactic:
have key := antitone_const_tsub.map_liminf_of_continuousAt (F := L)
    (fun i ↦ μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hne : L.NeBot
meas_Ec : (μ : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
meas_i_Ec :
  ∀ (i : ι),
    (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
key :
  HSub.hSub (α := ℝ≥0∞) 1 (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L) =
    limsup ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L
⊢ limsup ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
simpa [← key] using antitone_const_tsub h

Premises used: antitone_const_tsub
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_1 : IsProbabilityMeasure μ
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
compl_compl E ▸ limsup_measure_compl_le_of_le_liminf_measure (MeasurableSet.compl E_mble) h

Premises used: compl_compl, Eq.rec, MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
mp :
  (∀ (F : Set Ω),
      IsClosed[inst_1] F →
        LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)) →
    ∀ (G : Set Ω),
      IsOpen[inst_1] G →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
          (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
mpr :
  (∀ (G : Set Ω),
      IsOpen[inst_1] G →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
          (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)) →
    ∀ (F : Set Ω),
      IsClosed[inst_1] F →
        LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ (∀ (F : Set Ω),
      IsClosed[inst_1] F →
        LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)) ↔
    ∀ (G : Set Ω),
      IsOpen[inst_1] G →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
          (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (F : Set Ω),
    IsClosed[inst_1] F →
      LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
G : Set Ω
G_open : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)

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

Premises used: Iff.mpr, Compl.compl, IsOpen.measurableSet, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (F : Set Ω),
    IsClosed[inst_1] F →
      LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
G : Set Ω
G_open : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)

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

Premises used: Iff.mpr, Compl.compl, IsOpen.measurableSet, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)

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

Premises used: Iff.mpr, Compl.compl, IsClosed.measurableSet, MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl, isOpen_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) L : ℝ≥0∞)
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)

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

Premises used: Iff.mpr, Compl.compl, IsClosed.measurableSet, MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl, isOpen_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
hinf :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hsup :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
h :
  autoParam (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) L fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E)
    tendsto_of_le_liminf_of_limsup_le._auto_1
h' :
  autoParam (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) L fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E)
    tendsto_of_le_liminf_of_limsup_le._auto_3
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)

Tactic:
apply tendsto_of_le_liminf_of_limsup_le

Premises used: tendsto_of_le_liminf_of_limsup_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
⊢ E₀ =ᶠ[ae μ] E

Tactic:
have E₀_ae_eq_E : E₀ =ᵐ[μ] E :=
      EventuallyLE.antisymm E₀_subset.eventuallyLE
        (subset_E₁.eventuallyLE.trans (ae_le_set.mpr nulldiff))