awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
⊢ B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
have suffices : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j
Tactic: suffices B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Ici N, Es j) by
      refine this.trans <| union_subset_union le_rfl ?_
      intro ω hω
      simp only [mem_Ici, mem_iUnion, exists_prop] at hω
      obtain ⟨i, i_large, ω_in_Esi⟩ := hω
      by_contra con
      simp only [mem_Iio, compl_iUnion, mem_iInter, mem_compl_iff, not_forall, not_not,
                  exists_prop] at con
      obtain ⟨j, j_small, ω_in_Esj⟩ := con
      exact disjoint_left.mp (Es_disjoint (show j ≠ i by lia)) ω_in_Esj ω_in_Esi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
⊢ Membership.mem (γ := Set Ω) ((⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j) ω
have obtain : ∀ (i : ℕ) (hi : ω ∈ Es i), Membership.mem (γ := Set Ω) ((⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j) ω
Tactic: obtain ⟨i, hi⟩ := show ∃ n, ω ∈ Es n by simp only [← mem_iUnion, Es_cover, mem_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
i : ℕ
hi : ω ∈ Es i
⊢ Membership.mem (γ := Set Ω) ((⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j) ω
have simp : (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
Tactic: simp only [mem_Ici, mem_union, mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
i : ℕ
hi : ω ∈ Es i
⊢ (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
have pos : ∀ (i_small : i ∈ Iio N), (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
Tactic: by_cases i_small : i ∈ Iio N
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
i : ℕ
hi : ω ∈ Es i
pos : ∀ (i_small : i ∈ Iio N), (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
⊢ (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
have neg : ∀ (i_small : i ∉ Iio N), (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
Tactic: by_cases i_small : i ∈ Iio N
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
i : ℕ
hi : ω ∈ Es i
i_small : i ∈ Iio N
⊢ (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
have pos : i ∈ JB
Tactic: refine Or.inl ⟨i, ?_, self_subset_thickening third_ε_pos _ hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
ω : Ω
ω_in_B : ω ∈ B
i : ℕ
hi : ω ∈ Es i
i_small : i ∈ Iio N
⊢ i ∈ JB
have pos : (B ∩ Es i).Nonempty ∧ i < N
Tactic: simp only [mem_Iio, mem_setOf_eq, JB]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
⊢ ((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
Tactic: have B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ := by
    suffices B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Ici N, Es j) by
      refine this.trans <| union_subset_union le_rfl ?_
      intro ω hω
      simp only [mem_Ici, mem_iUnion, exists_prop] at hω
      obtain ⟨i, i_large, ω_in_Esi⟩ := hω
      by_contra con
      simp only [mem_Iio, compl_iUnion, mem_iInter, mem_compl_iff, not_forall, not_not,
                  exists_prop] at con
      obtain ⟨j, j_small, ω_in_Esj⟩ := con
      exact disjoint_left.mp (Es_disjoint (show j ≠ i by lia)) ω_in_Esj ω_in_Esi
    intro ω ω_in_B
    obtain ⟨i, hi⟩ := show ∃ n, ω ∈ Es n by simp only [← mem_iUnion, Es_cover, mem_univ]
    simp only [mem_Ici, mem_union, mem_iUnion, exists_prop]
    by_cases i_small : i ∈ Iio N
    · refine Or.inl ⟨i, ?_, self_subset_thickening third_ε_pos _ hi⟩
      simp only [mem_Iio, mem_setOf_eq, JB]
      exact ⟨Set.nonempty_of_mem <| mem_inter ω_in_B hi, i_small⟩
    · exact Or.inr ⟨i, by simpa only [mem_Iio, not_lt] using i_small, hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
ω : Ω
ω_in_U : Membership.mem (γ := Set Ω) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ω
⊢ ω ∈ thickening δ B
have ω_in_U₁ : ∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)
Tactic: simp only [mem_iUnion, exists_prop] at ω_in_U
Cleared hypotheses: ω_in_U
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
ω : Ω
ω_in_U : ∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)
⊢ ω ∈ thickening δ B
have obtain : ∀ (k : ℕ) (ω_in_thEk : ω ∈ thickening (ε / 3) (Es k)) (B_intersects : (B ∩ Es k).Nonempty),
  k ∈ Iio N → ω ∈ thickening δ B
Tactic: obtain ⟨k, ⟨B_intersects, _⟩, ω_in_thEk⟩ := ω_in_U
Cleared hypotheses: ω_in_U
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
ω : Ω
k : ℕ
ω_in_thEk : ω ∈ thickening (ε / 3) (Es k)
B_intersects : (B ∩ Es k).Nonempty
right : k ∈ Iio N
⊢ ω ∈ thickening δ B
have rw : ∀ (ω_in_thEk : ∃ z ∈ Es k, dist ω z < ε / 3) (B_intersects : (B ∩ Es k).Nonempty), k ∈ Iio N → ∃ z ∈ B, dist ω z < δ
Tactic: rw [mem_thickening_iff] at ω_in_thEk ⊢
Cleared hypotheses: ω_in_thEk, B_intersects, right