awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
apply : Ne (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (0 : ℝ≥0∞)
apply₁ : ε ≠ 0
⊢ HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)

Tactic:
apply lt_of_lt_of_le (ENNReal.sub_lt_self (by finiteness) _ _)
        <| ProbabilityMeasure.le_liminf_measure_open_of_tendsto tendsto_id G_open

Premises used: Filter.tendsto_id, MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, ENNReal.sub_lt_self, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
⊢ Ne (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(lt_of_lt_of_le ε_pos easy).ne.symm

Premises used: Ne.symm, lt_of_lt_of_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
⊢ Ne (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (lt_of_lt_of_le ε_pos easy).ne.symm

Premises used: Ne.symm, lt_of_lt_of_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
⊢ ε ≠ 0

Tactic:
ε_pos.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
⊢ ε ≠ 0

Tactic:
exact ε_pos.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
⊢ HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)

Tactic:
have aux : P.toMeasure G - ε < liminf (fun Q ↦ Q.toMeasure G) (𝓝 P) := by
    apply lt_of_lt_of_le (ENNReal.sub_lt_self (by finiteness) _ _)
        <| ProbabilityMeasure.le_liminf_measure_open_of_tendsto tendsto_id G_open
    · exact (lt_of_lt_of_le ε_pos easy).ne.symm
    · exact ε_pos.ne.symm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
aux :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)
h :
  ∀ (Q : ProbabilityMeasure Ω)
    (hQ :
      Membership.mem (γ := Set (ProbabilityMeasure Ω))
        (preimage (β := ℝ≥0∞) (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G)
          {x : ℝ≥0∞ | HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε < x})
        Q),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P

Tactic:
filter_upwards [gt_mem_sets_of_limsInf_gt (α := ℝ≥0∞) isBounded_ge_of_bot
      (show P.toMeasure G - ε < limsInf ((𝓝 P).map (fun Q ↦ Q.toMeasure G)) from aux)] with Q hQ

Premises used: Filter.isBounded_ge_of_bot, Filter.gt_mem_sets_of_limsInf_gt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
aux :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε < ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
⊢ HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε + ε <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε

Tactic:
ENNReal.add_lt_add_right ε_top hQ

Premises used: ENNReal.add_lt_add_right
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
aux :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε < ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
h :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G =
    HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε + ε
⊢ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G < HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε

Tactic:
convert! ENNReal.add_lt_add_right ε_top hQ

Premises used: ENNReal.add_lt_add_right
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
aux :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε < ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
⊢ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G =
    HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε + ε

Tactic:
(tsub_add_cancel_of_le easy).symm

Premises used: tsub_add_cancel_of_le, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
ε_top : ¬ε = ∞
aux :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ :
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε < ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
⊢ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G =
    HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε + ε

Tactic:
exact (tsub_add_cancel_of_le easy).symm

Premises used: tsub_add_cancel_of_le, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
inl :
  IsEmpty Ω →
    ∃ (As : ℕ → Set Ω),
      (∀ (n : ℕ), MeasurableSet (As n)) ∧
        (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
          (∀ (n : ℕ), diam (As n) ≤ ε) ∧
            Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)
inr :
  Nonempty Ω →
    ∃ (As : ℕ → Set Ω),
      (∀ (n : ℕ), MeasurableSet (As n)) ∧
        (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
          (∀ (n : ℕ), diam (As n) ≤ ε) ∧
            Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)
⊢ ∃ (As : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧
          Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
cases isEmpty_or_nonempty Ω

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : IsEmpty Ω
⊢ ∃ (As : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧
          Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_,
            fun _ _ _ ↦ disjoint_of_subsingleton⟩

Premises used: MeasurableSet.empty, Bornology.isBounded_empty, And.intro, Exists.intro, EmptyCollection.emptyCollection, disjoint_of_subsingleton
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : IsEmpty Ω
inl : ∀ (n : ℕ), diam.{u_1} (α := Ω) ((fun (x : ℕ) ↦ (∅ : Set Ω)) n) ≤ ε
inl₁ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set Ω)) n) univ
⊢ ∃ (As : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧
          Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
refine ⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_,
            fun _ _ _ ↦ disjoint_of_subsingleton⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : IsEmpty Ω
n : ℕ
⊢ diam.{u_1} (α := Ω) ((fun (x : ℕ) ↦ (∅ : Set Ω)) n) ≤ ε

Tactic:
simpa only [diam_empty] using ε_pos.le

Premises used: LT.lt.le, Metric.diam_empty
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : IsEmpty Ω
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set Ω)) n) univ

Tactic:
subsingleton
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
inr :
  ∀ (xs : ℕ → Ω) (xs_dense : DenseRange xs),
    ∃ (As : ℕ → Set Ω),
      (∀ (n : ℕ), MeasurableSet (As n)) ∧
        (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
          (∀ (n : ℕ), diam (As n) ≤ ε) ∧
            Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)
⊢ ∃ (As : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧
          Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
obtain ⟨xs, xs_dense⟩ := exists_dense_seq Ω

Premises used: TopologicalSpace.exists_dense_seq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
⊢ 0 < ε / 2

Tactic:
have half_ε_pos : 0 < ε / 2 := half_pos ε_pos
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ ∃ (As : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧
          Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
⟨As, ?_, ?_, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
inr : ∀ (n : ℕ), MeasurableSet (As n)
inr₁ : ∀ (n : ℕ), Bornology.IsBounded (As n)
inr₂ : ∀ (n : ℕ), diam (As n) ≤ ε
inr₃ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ
inr₄ : Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)
⊢ ∃ (As : ℕ → Set Ω),
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧
          Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ ∧ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ ∀ (n : ℕ), MeasurableSet (As n)

Tactic:
MeasurableSet.disjointed (fun n ↦ measurableSet_ball)

Premises used: measurableSet_ball, MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ ∀ (n : ℕ), MeasurableSet (As n)

Tactic:
exact MeasurableSet.disjointed (fun n ↦ measurableSet_ball)

Premises used: measurableSet_ball, MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ ∀ (n : ℕ), Bornology.IsBounded (As n)

Tactic:
fun n ↦ Bornology.IsBounded.subset isBounded_ball <| disjointed_subset Bs n

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset, disjointed_subset
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ ∀ (n : ℕ), Bornology.IsBounded (As n)

Tactic:
exact fun n ↦ Bornology.IsBounded.subset isBounded_ball <| disjointed_subset Bs n

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset, disjointed_subset
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
n : ℕ
inr : diam (Bs n) ≤ ε
⊢ diam (As n) ≤ ε

Tactic:
apply (diam_mono (disjointed_subset Bs n) isBounded_ball).trans

Premises used: Metric.isBounded_ball, Metric.diam_mono, disjointed_subset, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
n : ℕ
⊢ diam (ball (xs n) (ε / 2)) ≤ 2 * (ε / 2)

Tactic:
diam_ball half_ε_pos.le

Premises used: LT.lt.le, Metric.diam_ball
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h_1 : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
n : ℕ
h : ε = 2 * (ε / 2)
⊢ diam (Bs n) ≤ ε

Tactic:
convert! diam_ball half_ε_pos.le

Premises used: LT.lt.le, Metric.diam_ball
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
n : ℕ
⊢ ε = 2 * (ε / 2)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), UniformSpace.ball (xs i) {p : Ω × Ω | dist p.1 p.2 < ε / 2}) univ

Tactic:
DenseRange.iUnion_uniformity_ball xs_dense <| Metric.dist_mem_uniformity half_ε_pos

Premises used: DenseRange.iUnion_uniformity_ball, Metric.dist_mem_uniformity
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h_1 : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
h : ∀ (x : ℕ), Bs x = UniformSpace.ball (xs x) {p : Ω × Ω | dist p.1 p.2 < ε / 2}
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Bs n) univ

Tactic:
convert! DenseRange.iUnion_uniformity_ball xs_dense <| Metric.dist_mem_uniformity half_ε_pos

Premises used: DenseRange.iUnion_uniformity_ball, Metric.dist_mem_uniformity
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
x : ℕ
⊢ Bs x = UniformSpace.ball (xs x) {p : Ω × Ω | dist p.1 p.2 < ε / 2}

Tactic:
(ball_eq_ball' _ _).symm

Premises used: Eq.symm, Metric.ball_eq_ball'
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
x : ℕ
⊢ Bs x = UniformSpace.ball (xs x) {p : Ω × Ω | dist p.1 p.2 < ε / 2}

Tactic:
exact (ball_eq_ball' _ _).symm

Premises used: Eq.symm, Metric.ball_eq_ball'
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Bs n) univ

Tactic:
have aux : ⋃ n, Bs n = univ := by
      convert! DenseRange.iUnion_uniformity_ball xs_dense <| Metric.dist_mem_uniformity half_ε_pos
      exact (ball_eq_ball' _ _).symm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
aux : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Bs n) univ
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ

Tactic:
simpa only [← aux] using iUnion_disjointed

Premises used: iUnion_disjointed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
disjoint_disjointed Bs

Premises used: disjoint_disjointed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : (n : ℕ) → Set Ω := fun (n : ℕ) ↦ ball (xs n) (ε / 2)
As : (i : ℕ) → Set Ω := disjointed Bs
⊢ Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)

Tactic:
exact disjoint_disjointed Bs

Premises used: disjoint_disjointed