awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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}
this : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j
ω : Ω
i : ℕ
i_large : N ≤ i
ω_in_Esi : ω ∈ Es i
j : ℕ
j_small : j < N
ω_in_Esj : ω ∈ Es j
⊢ False

Tactic:
exact disjoint_left.mp (Es_disjoint (show j ≠ i by lia)) ω_in_Esj ω_in_Esi

Premises used: Set.disjoint_left, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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}
suffices : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j
⊢ B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio 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
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ ∃ (n : ℕ), ω ∈ Es n

Tactic:
simp only [← mem_iUnion, Es_cover, mem_univ]

Premises used: Set.mem_iUnion, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
obtain :
  ∀ (i : ℕ) (hi : ω ∈ Es i), Membership.mem (γ := Set Ω) ((⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j) ω
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
simp : (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i
⊢ Membership.mem (γ := Set Ω) ((⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j) ω

Tactic:
simp only [mem_Ici, mem_union, mem_iUnion, exists_prop]

Premises used: Set.mem_union, Set.mem_iUnion, exists_prop, Set.mem_Ici
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
neg : ∀ (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

Tactic:
by_cases i_small : i ∈ Iio N

Premises used: Set.Iio
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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

Tactic:
Or.inl ⟨i, ?_, self_subset_thickening third_ε_pos _ hi⟩

Premises used: And.intro, Metric.self_subset_thickening, Exists.intro, Or.inl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
pos : i ∈ JB
⊢ (∃ i ∈ JB, ω ∈ thickening (ε / 3) (Es i)) ∨ ∃ (i : ℕ), N ≤ i ∧ ω ∈ Es i

Tactic:
refine Or.inl ⟨i, ?_, self_subset_thickening third_ε_pos _ hi⟩

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
pos : (B ∩ Es i).Nonempty ∧ i < N
⊢ i ∈ JB

Tactic:
simp only [mem_Iio, mem_setOf_eq, JB]

Premises used: Set.mem_Iio, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ (B ∩ Es i).Nonempty ∧ i < N

Tactic:
⟨Set.nonempty_of_mem <| mem_inter ω_in_B hi, i_small⟩

Premises used: Set.mem_inter, And.intro, Set.nonempty_of_mem
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ (B ∩ Es i).Nonempty ∧ i < N

Tactic:
exact ⟨Set.nonempty_of_mem <| mem_inter ω_in_B hi, i_small⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ N ≤ i

Tactic:
simpa only [mem_Iio, not_lt] using i_small

Premises used: Set.mem_Iio, not_lt