awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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 : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have this : T.Nonempty
Tactic: have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have 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
Tactic: rcases T_count.exists_eq_range this with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have G_eq : G = ⋃ (n : ℕ), f n
Tactic: have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have this₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
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)
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have this₁ : Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
  (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)
Tactic: rw [← G_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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)
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have 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
Tactic: rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have refine_1 : r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ Finset.image f (Finset.range (n + 1)), t)
Tactic: refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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)
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have refine_2 : ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t ⊆ G
Tactic: refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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) (⋃ t ∈ Finset.image f (Finset.range (n + 1)), t)
have h₁ : ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t = accumulate f n
Tactic: convert! hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have obtain : ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
Tactic: classical
  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
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
have 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
Tactic: classical
  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
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = 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
have obtain₂ : ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty),
  ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
Tactic: classical
  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
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = 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
obtain₂ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty),
    ∃ (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
have obtain₃ : ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
  (hf : T = range f),
  ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
Tactic: classical
  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
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = 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
obtain₂ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₃ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (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
have obtain₄ : ∀ (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),
  ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
Tactic: classical
  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
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = 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
obtain₂ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₃ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₄ :
  ∀ (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),
    ∃ (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
have obtain₅ : ∀ (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)
  (this :
    Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ (i : ℕ), f i)) : Filter ℝ≥0)),
  ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
Tactic: classical
  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
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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)
⊢ Tendsto μ l (𝓝 ν)
have inl : ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥]
  (h' :
    ∀ s ∈ S,
      Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) ⊥
        (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)),
  Tendsto μ ⊥ (𝓝 ν)
Tactic: rcases l.eq_or_neBot with rfl | hl
Cleared hypotheses: l, inst_4, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
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 μ ⊥ (𝓝 ν)
⊢ Tendsto μ l (𝓝 ν)
have inr : ∀ (hl : l.NeBot), Tendsto μ l (𝓝 ν)
Tactic: rcases l.eq_or_neBot with rfl | hl