awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
this : G ⊆ ⋃ (i : (↑G : Type u_1)), interior (s i)
rw : Subset.{u_1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ y ∈ T₀, s y)
⊢ Subset.{u_1} (α := Set Ω) (⋃ (i : (↑G : Type u_1)), interior (s i)) (⋃ t ∈ s '' T₀, t)

Tactic:
rw [← hT₀, biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
this : G ⊆ ⋃ (i : (↑G : Type u_1)), interior (s i)
⊢ Subset.{u_1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ y ∈ T₀, s y)

Tactic:
iUnion₂_mono fun i j ↦ interior_subset

Premises used: interior_subset, Set.iUnion₂_mono
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
s : (x : (↑G : Type u_1)) → Set Ω
hsS : ∀ (x : (↑G : Type u_1)), s x ∈ S
hs_nhds : ∀ (x : (↑G : Type u_1)), s x ∈ 𝓝 (↑x : Ω)
hsG : ∀ (x : (↑G : Type u_1)), s x ⊆ G
T₀ : Set (↑G : Type u_1)
T₀_count : T₀.Countable
hT₀ : Eq.{u_1 + 1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ (i : (↑G : Type u_1)), interior (s i))
this : G ⊆ ⋃ (i : (↑G : Type u_1)), interior (s i)
⊢ Subset.{u_1} (α := Set Ω) (⋃ i ∈ T₀, interior (s i)) (⋃ y ∈ T₀, s y)

Tactic:
exact iUnion₂_mono fun i j ↦ interior_subset

Premises used: interior_subset, Set.iUnion₂_mono
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
obtain :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
obtain ⟨T, TS, T_count, hT⟩ : ∃ T : Set (Set Ω), T ⊆ S ∧ T.Countable ∧ ⋃ t ∈ T, t = G := by
    have : ∀ (x : G), ∃ s ∈ S, s ∈ 𝓝 (x : Ω) ∧ s ⊆ G := fun x ↦ h G hG x x.2
    choose! s hsS hs_nhds hsG using this
    rcases TopologicalSpace.isOpen_iUnion_countable (fun i ↦ interior (s i))
      (fun i ↦ isOpen_interior) with ⟨T₀, T₀_count, hT₀⟩
    refine ⟨s '' T₀, by grind, T₀_count.image s, ?_⟩
    refine Subset.antisymm (by simp; grind) ?_
    have : G ⊆ ⋃ i, interior (s i) := by
      intro y hy
      simpa using ⟨y, hy, mem_interior_iff_mem_nhds.2 (hs_nhds ⟨y, hy⟩)⟩
    apply this.trans
    rw [← hT₀, biUnion_image]
    exact iUnion₂_mono fun i j ↦ interior_subset

Premises used: Set
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
contrapose! : ∀ (hr : T = ∅), (ν : (a : Set Ω) → ℝ≥0) G ≤ r
⊢ T.Nonempty

Tactic:
contrapose! hr
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
hr : T = ∅
⊢ (ν : (a : Set Ω) → ℝ≥0) G ≤ r

Tactic:
simp [← hT, hr]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
⊢ T.Nonempty

Tactic:
have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this : T.Nonempty
rcases :
  ∀ (f : ℕ → Set Ω) (hf : T = range f),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
rcases T_count.exists_eq_range this with ⟨f, hf⟩

Premises used: Set.Countable.exists_eq_range
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
⊢ G = ⋃ (n : ℕ), f n

Tactic:
simp [← hT, hf]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
⊢ G = ⋃ (n : ℕ), f n

Tactic:
have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
⊢ Ne (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
⊢ ∀ (x : ℕ), Ne (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (accumulate f x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
⊢ Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ (i : ℕ), f i)) : Filter ℝ≥0)

Tactic:
have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ (i : ℕ), f i)) : Filter ℝ≥0)
⊢ Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)

Tactic:
rw [← G_eq] at this
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
rcases :
  ∀ (n : ℕ) (hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩

Premises used: tendsto_order, Filter.Eventually.exists, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
n : ℕ
hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)
⊢ ∀ t ∈ Finset.image f (Finset.range (n + 1)), t ∈ S

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
n : ℕ
hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)
refine_1 : r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ Finset.image f (Finset.range (n + 1)), t)
refine_2 : ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t ⊆ G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
n : ℕ
hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)
⊢ r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)

Tactic:
hn
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
n : ℕ
hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)
h₁ : ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t = accumulate f n
⊢ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ Finset.image f (Finset.range (n + 1)), t)

Tactic:
convert! hn
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
n : ℕ
hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)
⊢ ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t = accumulate f n

Tactic:
simp [accumulate_def]

Premises used: Set.accumulate_def
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this_1 : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ (n : ℕ), f n
this :
  Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
n : ℕ
hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)
⊢ ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t ⊆ G

Tactic:
simpa [G_eq] using fun i _ ↦ subset_iUnion f i

Premises used: Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥]
    (h' :
      ∀ s ∈ S,
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) ⊥
          (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)),
    Tendsto μ ⊥ (𝓝 ν)
inr : ∀ (hl : l.NeBot), Tendsto μ l (𝓝 ν)
⊢ Tendsto μ l (𝓝 ν)

Tactic:
rcases l.eq_or_neBot with rfl | hl

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
inst_4 : IsCountablyGenerated.{u_2} (α := ι) ⊥
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) ⊥
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
⊢ Tendsto μ ⊥ (𝓝 ν)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
inr :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ι) ↦ (μ i : (a : Set Ω) → ℝ≥0) G) l : ℝ≥0)
⊢ Tendsto μ l (𝓝 ν)

Tactic:
apply tendsto_of_forall_isOpen_le_liminf

Premises used: MeasureTheory.tendsto_of_forall_isOpen_le_liminf
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
⊢ ∀ (i : ι), LE.le (α := ℝ≥0) ((μ i : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (1 : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) l fun (i : ι) ↦ (μ i : (a : Set Ω) → ℝ≥0) G

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
inr : ∀ (r : ℝ≥0) (hr : r < (ν : (a : Set Ω) → ℝ≥0) G), ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
⊢ LE.le (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ι) ↦ (μ i : (a : Set Ω) → ℝ≥0) G) l : ℝ≥0)

Tactic:
refine (le_liminf_iff (isCoboundedUnder_ge_of_le (x := 1) l (by simp)) (by isBoundedDefault)).2
    (fun r hr ↦ ?_)

Premises used: Iff.mpr, Filter.isCoboundedUnder_ge_of_le, Filter.le_liminf_iff
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
ν.exists_lt_measure_biUnion_of_isOpen h hG hr

Premises used: MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
inr :
  ∀ (T : Finset (Set Ω)) (TS : ∀ t ∈ T, t ∈ S) (T_meas : r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t))
    (TG : ⋃ t ∈ T, t ⊆ G), ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
⊢ ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G

Tactic:
obtain ⟨T, TS, T_meas, TG⟩ :
      ∃ T : Finset (Set Ω), (∀ t ∈ T, t ∈ S) ∧ (r < ν (⋃ t ∈ T, t)) ∧ (⋃ t ∈ T, t) ⊆ G :=
    ν.exists_lt_measure_biUnion_of_isOpen h hG hr

Premises used: MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen, Finset, Set