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}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
⊢ ⋃ 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
-- 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}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
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 δ)
⊢ ((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) B ≤
    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 ?_)

Premises used: MeasureTheory.measure_mono, LE.le.trans, MeasureTheory.measure_union_le
-- 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}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
⊢ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))

Tactic:
specialize hQ _ (show JB ⊆ Iio N from fun _ h ↦ h.2)

Premises used: And.right
-- 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 Ω
δ : ℝ
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
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
apply :
  HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3)) +
      ENNReal.ofReal (ε / 3) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
⊢ 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 (add_le_add hQ.le hN.le).trans

Premises used: add_le_add, LT.lt.le, LE.le.trans
-- 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 Ω
δ : ℝ
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
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
rw :
  HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (2 * (ε / 3))) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
⊢ HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3)) +
      ENNReal.ofReal (ε / 3) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)

Tactic:
rw [add_assoc, ← ENNReal.ofReal_add third_ε_pos.le third_ε_pos.le, ← two_mul]

Premises used: add_assoc, two_mul, LT.lt.le, ENNReal.ofReal_add
-- 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 Ω
δ : ℝ
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
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
apply : 2 * (ε / 3) ≤ δ
⊢ HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (2 * (ε / 3))) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)

Tactic:
apply add_le_add (measure_mono subset_thickB) (ofReal_le_ofReal _)

Premises used: add_le_add, ENNReal.ofReal_le_ofReal, MeasureTheory.measure_mono
-- 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 Ω
δ : ℝ
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
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
⊢ 2 * (ε / 3) ≤ δ

Tactic:
δ_gt.le

Premises used: LT.lt.le
-- 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 Ω
δ : ℝ
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
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
⊢ 2 * (ε / 3) ≤ δ

Tactic:
exact δ_gt.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
s : Set (ProbabilityMeasure Ω)
hs : IsOpen[coinduced toMeasure inferInstance] s
⊢ IsOpen[inferInstance] s

Tactic:
simpa using hs.preimage continuous_ofMeasure_probabilityMeasure

Premises used: MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure, IsOpen.preimage
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
X : Type u_2
inst_4 : TopologicalSpace X
inst_5 : PseudoMetrizableSpace X
inst_6 : SeparableSpace X
inst_7 : MeasurableSpace X
inst_8 : OpensMeasurableSpace X
⊢ PseudoMetrizableSpace.{u_2} (ProbabilityMeasure X)

Tactic:
letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
  (LevyProkhorov.probabilityMeasureHomeomorph (Ω := X)).isInducing.pseudoMetrizableSpace

Premises used: Homeomorph.isInducing, Topology.IsInducing.pseudoMetrizableSpace, MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
X : Type u_2
inst_4 : TopologicalSpace X
inst_5 : PseudoMetrizableSpace X
inst_6 : SeparableSpace X
inst_7 : MeasurableSpace X
inst_8 : BorelSpace X
this : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ MetrizableSpace.{u_2} (ProbabilityMeasure X)

Tactic:
LevyProkhorov.probabilityMeasureHomeomorph.isEmbedding.metrizableSpace

Premises used: Topology.IsEmbedding.metrizableSpace, Homeomorph.isEmbedding, MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorph
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
X : Type u_2
inst_4 : TopologicalSpace X
inst_5 : PseudoMetrizableSpace X
inst_6 : SeparableSpace X
inst_7 : MeasurableSpace X
inst_8 : BorelSpace X
this : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ MetrizableSpace.{u_2} (ProbabilityMeasure X)

Tactic:
exact LevyProkhorov.probabilityMeasureHomeomorph.isEmbedding.metrizableSpace
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ llr μ ν = fun (x : α) ↦ log (μ.rnDeriv ν x).toReal

Tactic:
rfl

Premises used: MeasureTheory.llr, rfl
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
a : α
ha : μ.rnDeriv μ a = 1
⊢ llr μ μ a = 0 a

Tactic:
simp [llr, ha]

Premises used: MeasureTheory.llr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv μ x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ llr μ μ x = 0 x) x} x}
      a
h₁ h₂ : ∀ (a : α) (ha : μ.rnDeriv μ a = 1), llr μ μ a = 0 a
⊢ llr μ μ =ᶠ[ae μ] 0

Tactic:
filter_upwards [μ.rnDeriv_self] with a ha using by simp [llr, ha]

Premises used: MeasureTheory.Measure.rnDeriv_self
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
h : ∀ (x : α) (hx : μ.rnDeriv ν x < ∞), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (llr μ ν x)) fun (x : α) ↦
    if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx

Premises used: MeasureTheory.Measure.rnDeriv_lt_top
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
pos : ∀ (h_zero : μ.rnDeriv ν x = 0), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
neg : ∀ (h_zero : ¬μ.rnDeriv ν x = 0), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
by_cases h_zero : μ.rnDeriv ν x = 0

Premises used: MeasureTheory.Measure.rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : μ.rnDeriv ν x = 0
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
simp only [llr, h_zero, ENNReal.toReal_zero, log_zero, exp_zero, ite_true]

Premises used: MeasureTheory.llr, ite_true, ENNReal.toReal_zero, Real.exp_zero, Real.log_zero
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
neg : 0 < (μ.rnDeriv ν x).toReal
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
rw [llr, exp_log, if_neg h_zero]

Premises used: MeasureTheory.llr, Real.exp_log, if_neg
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ 0 < (μ.rnDeriv ν x).toReal

Tactic:
ENNReal.toReal_pos h_zero hx.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ 0 < (μ.rnDeriv ν x).toReal

Tactic:
exact ENNReal.toReal_pos h_zero hx.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne