awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
key :
  Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
obs :
  Tendsto (β := ℝ≥0∞)
    (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) x) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
ε : ℝ≥0∞
ε_pos : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) ε
⊢ (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞) ε

Tactic:
exact left_measure_le_of_levyProkhorovEDist_lt (B_mble := s_mble) (hLP ▸ ε_pos)

Premises used: MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
a₁ : LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
      hLP s_closed.measurableSet hνs |>.trans <|
      le_of_eq (congr_arg _ s_closed.closure_eq)

Premises used: IsClosed.closure_eq, IsClosed.measurableSet, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, congr_arg, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
      hLP s_closed.measurableSet hνs |>.trans <|
      le_of_eq (congr_arg _ s_closed.closure_eq)

Premises used: IsClosed.closure_eq, IsClosed.measurableSet, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, congr_arg, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
      (levyProkhorovEDist_comm μ ν ▸ hLP) s_closed.measurableSet hμs |>.trans <|
      le_of_eq (congr_arg _ s_closed.closure_eq)

Premises used: IsClosed.closure_eq, IsClosed.measurableSet, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, congr_arg, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
      (levyProkhorovEDist_comm μ ν ▸ hLP) s_closed.measurableSet hμs |>.trans <|
      le_of_eq (congr_arg _ s_closed.closure_eq)

Premises used: IsClosed.closure_eq, IsClosed.measurableSet, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, congr_arg, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
apply :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
apply levyProkhorovEDist_le_of_forall μ ν δ

Premises used: MeasureTheory.levyProkhorovEDist_le_of_forall
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
    (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
⟨h ε B ε_gt ε_lt_top B_mble, ?_⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
refine : (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
    (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
refine ⟨h ε B ε_gt ε_lt_top B_mble, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ

Tactic:
have B_subset := subset_compl_thickening_compl_thickening_self ε.toReal B
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
apply :
  (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
apply (measure_mono (μ := ν) B_subset).trans

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet]

Premises used: Metric.isOpen_thickening, IsOpen.measurableSet, MeasureTheory.prob_compl_eq_one_sub
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
⊢ MeasurableSet (thickening ε.toReal B)ᶜ

Tactic:
have Tc_mble := (isOpen_thickening (δ := ε.toReal) (E := B)).isClosed_compl.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B)ᶜ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε

Tactic:
specialize h ε (thickening ε.toReal B)ᶜ ε_gt ε_lt_top Tc_mble

Premises used: Compl.compl, Metric.thickening, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h :
  (μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B)ᶜ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε

Tactic:
rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet] at h

Premises used: Metric.isOpen_thickening, IsOpen.measurableSet, MeasureTheory.prob_compl_eq_one_sub
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε
⊢ HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε)
      ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞)

Tactic:
have almost := add_le_add (c := μ (thickening ε.toReal B)) h rfl.le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε
almost :
  HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞))
      ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε)
      ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞)
⊢ 1 ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞)
      (HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞))

Tactic:
rw [tsub_add_cancel_of_le prob_le_one, add_assoc] at almost

Premises used: add_assoc, MeasureTheory.prob_le_one, tsub_add_cancel_of_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε
almost :
  1 ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞)
      (HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞))
apply :
  HSub.hSub (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞)
        (HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞)))
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
apply (tsub_le_tsub_right almost _).trans

Premises used: tsub_le_tsub_right, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ε
almost :
  1 ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞)
      (HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞))
rw :
  HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ HSub.hSub (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞)
        (HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞)))
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
rw [ENNReal.add_sub_cancel_left (measure_ne_top ν _), add_comm ε]

Premises used: ENNReal.add_sub_cancel_left, MeasureTheory.measure_ne_top, add_comm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h :
  ∀ (ε : ℝ) (B : Set Ω),
    δ < ε →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
          HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε B) : ℝ≥0∞) (ENNReal.ofReal ε)
apply : levyProkhorovEDist μ ν ≤ ENNReal.ofReal δ
⊢ levyProkhorovDist μ ν ≤ δ

Tactic:
apply toReal_le_of_le_ofReal δ_nn

Premises used: ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h :
  ∀ (ε : ℝ) (B : Set Ω),
    δ < ε →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
          HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε B) : ℝ≥0∞) (ENNReal.ofReal ε)
h₁ :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    ENNReal.ofReal δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ levyProkhorovEDist μ ν ≤ ENNReal.ofReal δ

Tactic:
apply levyProkhorovEDist_le_of_forall_le

Premises used: MeasureTheory.levyProkhorovEDist_le_of_forall_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h :
  ∀ (ε : ℝ) (B : Set Ω),
    δ < ε →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
          HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε B) : ℝ≥0∞) (ENNReal.ofReal ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ δ < ε.toReal

Tactic:
(ofReal_lt_ofReal_iff ?_).mp ?_

Premises used: Iff.mp, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h :
  ∀ (ε : ℝ) (B : Set Ω),
    δ < ε →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
          HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε B) : ℝ≥0∞) (ENNReal.ofReal ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
refine_1 : 0 < ε.toReal
refine_2 : ENNReal.ofReal δ < ENNReal.ofReal ε.toReal
⊢ δ < ε.toReal

Tactic:
refine (ofReal_lt_ofReal_iff ?_).mp ?_

Premises used: Iff.mp, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h :
  ∀ (ε : ℝ) (B : Set Ω),
    δ < ε →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
          HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε B) : ℝ≥0∞) (ENNReal.ofReal ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ 0 < ε.toReal

Tactic:
ENNReal.toReal_pos ε_gt.bot_lt.ne' ε_lt_top.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne', LT.lt.bot_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h :
  ∀ (ε : ℝ) (B : Set Ω),
    δ < ε →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
          HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε B) : ℝ≥0∞) (ENNReal.ofReal ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ 0 < ε.toReal

Tactic:
exact ENNReal.toReal_pos ε_gt.bot_lt.ne' ε_lt_top.ne

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