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_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
ω : Ω
k : ℕ
ω_in_thEk : ∃ z ∈ Es k, dist ω z < ε / 3
B_intersects : (B ∩ Es k).Nonempty
right : k ∈ Iio N
⊢ ∃ z ∈ B, dist ω z < δ
have obtain : ∀ (w : Ω) (w_in_Ek : w ∈ Es k) (w_near : dist ω w < ε / 3), ∃ z ∈ B, dist ω z < δ
Tactic: obtain ⟨w, w_in_Ek, w_near⟩ := ω_in_thEk
Cleared hypotheses: ω_in_thEk
-- 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 : ℕ
B_intersects : (B ∩ Es k).Nonempty
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
⊢ ∃ z ∈ B, dist ω z < δ
have obtain : ∀ (z : Ω) (z_in_B : z ∈ B) (z_in_Ek : z ∈ Es k), ∃ z ∈ B, dist ω z < δ
Tactic: obtain ⟨z, ⟨z_in_B, z_in_Ek⟩⟩ := B_intersects
Cleared hypotheses: B_intersects
-- 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 : ℕ
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
z : Ω
z_in_B : z ∈ B
z_in_Ek : z ∈ Es k
⊢ ∃ z ∈ B, dist ω z < δ
have refine : dist ω w + dist w z < δ
Tactic: refine ⟨z, z_in_B, lt_of_le_of_lt (dist_triangle ω w z) ?_⟩
-- 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 : ℕ
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
z : Ω
z_in_B : z ∈ B
z_in_Ek : z ∈ Es k
⊢ dist ω w + dist w z < δ
have apply : ε / 3 + ε / 3 < δ
Tactic: apply lt_of_le_of_lt (add_le_add w_near.le <|
            (dist_le_diam_of_mem (Es_bdd k) w_in_Ek z_in_Ek).trans <| Es_diam k)
-- 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 : ℕ
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
z : Ω
z_in_B : z ∈ B
z_in_Ek : z ∈ Es k
⊢ ε / 3 + ε / 3 < δ
have linarith : δ ≤ ε / 3 + ε / 3 → 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
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 : ℕ
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
z : Ω
z_in_B : z ∈ B
z_in_Ek : z ∈ Es k
linarith : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
⊢ ε / 3 + ε / 3 < δ
have linarith₁ : δ ≤ ε / 3 + ε / 3 → 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
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 : ℕ
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
z : Ω
z_in_B : z ∈ B
z_in_Ek : z ∈ Es k
linarith : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₁ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₃ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ ε / 3 + ε / 3 < δ
have linarith₄ : δ ≤ ε / 3 + ε / 3 → 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
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 : ℕ
right : k ∈ Iio N
w : Ω
w_in_Ek : w ∈ Es k
w_near : dist ω w < ε / 3
z : Ω
z_in_B : z ∈ B
z_in_Ek : z ∈ Es k
linarith : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₁ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₃ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₄ : δ ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 3 0
linarith₅ : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₆ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₇ : δ ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 3 0
linarith₈ : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₉ linarith₁₀ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₁ : δ ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 3 0
linarith₁₂ : δ ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₁₃ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₄ : δ ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 3 0
⊢ ε / 3 + ε / 3 < δ
have linarith₁₅ : δ ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 2 * (1 * ε) - 3 * δ + (3 * δ - (1 * ε + 1 * ε)) = 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
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)ᶜ
⊢ ((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
Tactic: have subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B := by
    intro ω ω_in_U
    simp only [mem_iUnion, exists_prop] at ω_in_U
    obtain ⟨k, ⟨B_intersects, _⟩, ω_in_thEk⟩ := ω_in_U
    rw [mem_thickening_iff] at ω_in_thEk ⊢
    obtain ⟨w, w_in_Ek, w_near⟩ := ω_in_thEk
    obtain ⟨z, ⟨z_in_B, z_in_Ek⟩⟩ := B_intersects
    refine ⟨z, z_in_B, lt_of_le_of_lt (dist_triangle ω w z) ?_⟩
    apply lt_of_le_of_lt (add_le_add w_near.le <|
            (dist_le_diam_of_mem (Es_bdd k) w_in_Ek z_in_Ek).trans <| Es_diam k)
    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
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)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
⊢ ((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have apply : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    (((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
    (((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
    (ENNReal.ofReal δ)
Tactic: apply (measure_mono B_subset).trans ((measure_union_le _ _).trans ?_)