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 Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
pos :
  ∀ (ε_top : ε = ∞),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
      𝓝 P
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
have neg : ∀ (ε_top : ¬ε = ∞),
  {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
Tactic: by_cases ε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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)
have apply : Ne (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply lt_of_lt_of_le (ENNReal.sub_lt_self (by finiteness) _ _)
        <| ProbabilityMeasure.le_liminf_measure_open_of_tendsto tendsto_id G_open
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞)
⊢ HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε <
    liminf (fun (Q : ProbabilityMeasure Ω) ↦ ((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) (𝓝 P)
have apply₁ : ε ≠ 0
Tactic: apply lt_of_lt_of_le (ENNReal.sub_lt_self (by finiteness) _ _)
        <| ProbabilityMeasure.le_liminf_measure_open_of_tendsto tendsto_id G_open
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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 : ¬ε = ∞
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
have aux : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
have 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∞) ε
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 < HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε
have h : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G =
  HSub.hSub (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε + ε
Tactic: convert! ENNReal.add_lt_add_right ε_top hQ
-- 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 Ω
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ (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)
have 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)
Tactic: cases isEmpty_or_nonempty Ω
-- 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 Ω
ε : ℝ
ε_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)
⊢ ∃ (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)
have 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)
Tactic: cases isEmpty_or_nonempty Ω
-- 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 Ω
ε : ℝ
ε_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)
have inl : ∀ (n : ℕ), diam.{u_1} (α := Ω) ((fun (x : ℕ) ↦ (∅ : Set Ω)) n) ≤ ε
Tactic: refine ⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_,
            fun _ _ _ ↦ disjoint_of_subsingleton⟩
-- 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 Ω
ε : ℝ
ε_pos : 0 < ε
h : IsEmpty Ω
inl : ∀ (n : ℕ), diam.{u_1} (α := Ω) ((fun (x : ℕ) ↦ (∅ : Set Ω)) n) ≤ ε
⊢ ∃ (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)
have inl₁ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set Ω)) n) univ
Tactic: refine ⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_,
            fun _ _ _ ↦ disjoint_of_subsingleton⟩
-- 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 Ω
ε : ℝ
ε_pos : 0 < ε
h : 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)
have 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)
Tactic: obtain ⟨xs, xs_dense⟩ := exists_dense_seq Ω
-- 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 Ω
ε : ℝ
ε_pos : 0 < ε
h : Nonempty Ω
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)
have half_ε_pos : 0 < ε / 2
Tactic: have half_ε_pos : 0 < ε / 2 := half_pos ε_pos
-- 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 Ω
ε : ℝ
ε_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)
have inr : ∀ (n : ℕ), MeasurableSet (As n)
Tactic: refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
-- 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 Ω
ε : ℝ
ε_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)
⊢ ∃ (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)
have inr₁ : ∀ (n : ℕ), Bornology.IsBounded (As n)
Tactic: refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
-- 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 Ω
ε : ℝ
ε_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)
⊢ ∃ (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)
have inr₂ : ∀ (n : ℕ), diam (As n) ≤ ε
Tactic: refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
-- 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 Ω
ε : ℝ
ε_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) ≤ ε
⊢ ∃ (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)
have inr₃ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), As n) univ
Tactic: refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
-- 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 Ω
ε : ℝ
ε_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
⊢ ∃ (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)
have inr₄ : Pairwise fun (n m : ℕ) ↦ Disjoint (As n) (As m)
Tactic: refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
-- 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 Ω
ε : ℝ
ε_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 (As n) ≤ ε
have inr : diam (Bs n) ≤ ε
Tactic: apply (diam_mono (disjointed_subset Bs n) isBounded_ball).trans
-- 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 Ω
ε : ℝ
ε_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 (Bs n) ≤ ε
have h : ε = 2 * (ε / 2)
Tactic: convert! diam_ball half_ε_pos.le
-- 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 Ω
ε : ℝ
ε_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
have h : ∀ (x : ℕ), Bs x = UniformSpace.ball (xs x) {p : Ω × Ω | dist p.1 p.2 < ε / 2}
Tactic: convert! DenseRange.iUnion_uniformity_ball xs_dense <| Metric.dist_mem_uniformity half_ε_pos
-- 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 Ω
ε : ℝ
ε_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 : ℕ), As n) univ
have aux : 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
-- 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 Ω
⊢ Continuous[ProbabilityMeasure.instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ofMeasure
have rw : ∀ (x : ProbabilityMeasure Ω), ContinuousAt ofMeasure x
Tactic: rw [continuous_iff_continuousAt]
-- 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 Ω
⊢ ContinuousAt ofMeasure P
have rw : ∀ ε > 0, ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Tactic: rw [continuousAt_iff']
-- 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
⊢ 0 < ε / 3
have linarith : ε / 3 ≤ 0 → 3 / 3 = 1
Tactic: linarith
-- 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
linarith : ε / 3 ≤ 0 → 3 / 3 = 1
⊢ 0 < ε / 3
have linarith₁ : ε / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith
-- 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
linarith : ε / 3 ≤ 0 → 3 / 3 = 1
linarith₁ : ε / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ 0 < ε / 3
have linarith₂ : ε / 3 ≤ 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- 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
linarith : ε / 3 ≤ 0 → 3 / 3 = 1
linarith₁ : ε / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ε / 3 ≤ 0 → GT.gt (α := ℝ) 3 0
⊢ 0 < ε / 3
have linarith₃ : ε / 3 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 3 0) = 0
Tactic: linarith
-- 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
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
have third_ε_pos : 0 < ε / 3
Tactic: have third_ε_pos : 0 < ε / 3 := by linarith
-- 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
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
have third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Tactic: have third_ε_pos' : 0 < ENNReal.ofReal (ε / 3) := ofReal_pos.mpr third_ε_pos
-- 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)
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
have obtain : ∀ (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)),
  ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Tactic: obtain ⟨Es, Es_mble, Es_bdd, Es_diam, Es_cover, Es_disjoint⟩ :=
    SeparableSpace.exists_measurable_partition_diam_le Ω third_ε_pos
-- 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 : ℕ), ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
have exhaust : Tendsto (α := ℕ) (β := ℝ≥0∞)
  (Function.comp (β := Set Ω) (⇑(↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i)
  atTop (𝓝 0)
Tactic: have exhaust := @tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint Ω _ P.toMeasure _
                    Es (fun n ↦ (Es_mble n).nullMeasurableSet) Es_disjoint
-- 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)
exhaust :
  Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set Ω) (⇑(↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i)
    atTop (𝓝 0)
⊢ ∃ (N : ℕ), ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
have exhaust₁ : ∀ (U : Set ℝ≥0∞),
  0 ∈ U →
    IsOpen U →
      ∃ (N : ℕ),
        ∀ (n : ℕ),
          N ≤ n →
            Membership.mem (α := ℝ≥0∞) U
              (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) : ℝ≥0∞)
Tactic: simp only [tendsto_atTop_nhds, Function.comp_apply] at exhaust
Cleared hypotheses: exhaust