awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
have obs : Tendsto (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) (id x))
  (𝓝[>] 0)
  (𝓝
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞) (0 : ℝ≥0∞)))
Tactic: have obs := Tendsto.add key (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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 (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) (id x))
    (𝓝[>] 0)
    (𝓝
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞) (0 : ℝ≥0∞)))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
have 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∞)
Tactic: simp only [id_eq, add_zero] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
have apply : ∀ᶠ (c : ℝ≥0∞) in 𝓝[>] 0,
  (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal s) : ℝ≥0∞) c
Tactic: apply ge_of_tendsto (b := μ s) obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞)
⊢ ∀ᶠ (c : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal s) : ℝ≥0∞) c
have h : ∀ (ε : ℝ≥0∞) (ε_pos : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) ε),
  (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞) ε
Tactic: filter_upwards [self_mem_nhdsWithin] with ε ε_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞) ε
⊢ levyProkhorovEDist μ ν ≤ δ
have 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∞) ε
Tactic: apply levyProkhorovEDist_le_of_forall μ ν δ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞) ε
have refine : (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
Tactic: refine ⟨h ε B ε_gt ε_lt_top B_mble, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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∞) ε
have B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tactic: have B_subset := subset_compl_thickening_compl_thickening_self ε.toReal B
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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)ᶜ)ᶜ
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
have apply : (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
Tactic: apply (measure_mono (μ := ν) B_subset).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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)ᶜ)ᶜ
⊢ (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
have 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∞) ε
Tactic: rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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)ᶜ)ᶜ
⊢ 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∞) ε
have Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
Tactic: have Tc_mble := (isOpen_thickening (δ := ε.toReal) (E := B)).isClosed_compl.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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)ᶜ
⊢ 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∞) ε
have h₁ : (μ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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 (thickening ε.toReal B)ᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
have 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∞) ε
Tactic: rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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∞) ε
⊢ 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∞) ε
have 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∞)
Tactic: have almost := add_le_add (c := μ (thickening ε.toReal B)) h rfl.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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∞)
⊢ 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∞) ε
have almost₁ : 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
Cleared hypotheses: almost
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞))
⊢ 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∞) ε
have 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∞) ε
Tactic: apply (tsub_le_tsub_right almost _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞))
⊢ 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∞) ε
have rw : HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set Ω) → ℝ≥0∞) (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 ε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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∞) ε
⊢ 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∞) ε
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (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 ε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ε)
⊢ levyProkhorovDist μ ν ≤ δ
have apply : levyProkhorovEDist μ ν ≤ ENNReal.ofReal δ
Tactic: apply toReal_le_of_le_ofReal δ_nn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ε)
⊢ levyProkhorovEDist μ ν ≤ ENNReal.ofReal δ
have h₁ : ∀ (ε : ℝ≥0∞) (B : Set Ω),
  ENNReal.ofReal δ < ε →
    ε < ∞ →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
Tactic: apply levyProkhorovEDist_le_of_forall_le