awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ EqOn f g U
have this : IsOpen[inst] (U ∩ {a : X | f a ≠ g a})
Tactic: have : IsOpen (U ∩ { a | f a ≠ g a }) := by
    refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_
    rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
    exact
      (hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))
        (isClosed_diagonal.isOpen_compl.mem_nhds ha')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IsOpen[inst] (U ∩ {a : X | f a ≠ g a})
⊢ EqOn f g U
have this₁ : U ∩ {a : X | f a ≠ g a} ≤ ∅
Tactic: replace := (this.eq_empty_of_measure_zero h).le
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
⊢ IsOpenPosMeasure (m := inst_4) (map f μ)
have refine : ∀ (U : Set Z) (hUo : IsOpen[inst_3] U) (hUne : U.Nonempty),
  Ne (α := ℝ≥0∞) (((map f μ : Measure Z) : (a : Set Z) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨fun U hUo hUne => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen[inst_3] U
hUne : U.Nonempty
⊢ Ne (α := ℝ≥0∞) (((map f μ : Measure Z) : (a : Set Z) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (f ⁻¹' U) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply hf.measurable hUo.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : BorelSpace X
Z : Type u_3
inst_2 : TopologicalSpace Z
mZ : MeasurableSpace Z
inst_3 : BorelSpace Z
μ : Measure Z
inst_4 : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst] U
Une : U.Nonempty
⊢ Ne (α := ℝ≥0∞) (((comap f μ : Measure X) : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) ((μ : (a : Set Z) → ℝ≥0∞) (f '' U) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hf.measurableEmbedding.comap_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ↔ 0 < r
have refine : ∀ (h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)), 0 < r
Tactic: refine ⟨fun h ↦ ?_, measure_closedBall_pos μ x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ 0 < r
have contrapose! : ∀ (h : r ≤ 0), LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
h : r ≤ 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) 0 0
Tactic: rw [(subsingleton_closedBall x h).measure_zero μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₁s : IsSigmaCompact s
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsMeagre s
have rcases : ∀ (K : ℕ → Set X) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hcover : ⋃ (n : ℕ), K n = s), IsMeagre s
Tactic: rcases h₁s with ⟨K, hcompact, hcover⟩
Cleared hypotheses: h₁s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
n : ℕ
⊢ IsNowhereDense (K n)
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (K n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
⊢ IsMeagre s
have h : ∀ (n : ℕ), IsNowhereDense (K n)
Tactic: have h (n : ℕ) : IsNowhereDense (K n) := by
    have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
    exact .of_isClosed_null (hcompact n).isClosed this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ IsMeagre s
have rw : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Tactic: rw [isMeagre_iff_countable_union_isNowhereDense]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
have 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∞)
Tactic: rcases L.eq_or_neBot with rfl | hne
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
have inr : ∀ (hne : L.NeBot),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
have meas_Ec : (μ : (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
have meas_i_Ec : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
have 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
Tactic: simp_rw [meas_Ec, meas_i_Ec]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) ≤
    liminf ((fun (x : ℝ≥0∞) ↦ 1 - x) ∘ fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
have 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∞)
Tactic: rcases L.eq_or_neBot with rfl | hne
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
have inr : ∀ (hne : L.NeBot),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
have meas_Ec : (μ : (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
have meas_i_Ec : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) Eᶜ) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Eᶜ : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [meas_Ec, meas_i_Ec]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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∞)
⊢ 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∞)
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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)
⊢ (∀ (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∞)
have 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∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ (∀ (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∞)
have 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∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
have hinf : LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
Tactic: apply tendsto_of_le_liminf_of_limsup_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
have hsup : LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
Tactic: apply tendsto_of_le_liminf_of_limsup_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
have 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
Tactic: apply tendsto_of_le_liminf_of_limsup_le