awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ δ < ε.toReal
have refine_1 : 0 < ε.toReal
Tactic: refine (ofReal_lt_ofReal_iff ?_).mp ?_
-- 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 ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
refine_1 : 0 < ε.toReal
⊢ δ < ε.toReal
have refine_2 : ENNReal.ofReal δ < ENNReal.ofReal ε.toReal
Tactic: refine (ofReal_lt_ofReal_iff ?_).mp ?_
-- 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 ν
δ : ℝ
δ_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
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
have ε_gt' : δ < ε.toReal
Tactic: have ε_gt' : δ < ε.toReal := by
    refine (ofReal_lt_ofReal_iff ?_).mp ?_
    · exact ENNReal.toReal_pos ε_gt.bot_lt.ne' ε_lt_top.ne
    · simpa [ofReal_toReal_eq_iff.mpr ε_lt_top.ne] using ε_gt
-- 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 ε)
ε : ℝ≥0∞
B : Set Ω
ε_gt : ENNReal.ofReal δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
ε_gt' : δ < ε.toReal
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
have h₁ : ε = ENNReal.ofReal ε.toReal
Tactic: convert! h ε.toReal B ε_gt' B_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ μ = ν
have a : μ.toMeasure = ν.toMeasure
Tactic: apply toMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ μ.toMeasure = ν.toMeasure
have a : (↑μ.toMeasure : Measure Ω) = (↑ν.toMeasure : Measure Ω)
Tactic: apply ProbabilityMeasure.toMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ (↑μ.toMeasure : Measure Ω) = (↑ν.toMeasure : Measure Ω)
have a : inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
Tactic: refine ext_of_generate_finite _ ?_ isPiSystem_isClosed (fun A hA ↦ ?_) (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
a : inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
⊢ (↑μ.toMeasure : Measure Ω) = (↑ν.toMeasure : Measure Ω)
have a₁ : ∀ (A : Set Ω)
  (hA :
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} A),
  Eq (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
    (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: refine ext_of_generate_finite _ ?_ isPiSystem_isClosed (fun A hA ↦ ?_) (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
have a : borel Ω = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
Tactic: rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
a :
  borel Ω = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
⊢ inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
have a₁ : Eq.{u_1 + 1} (α := MeasurableSpace Ω)
  (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s})
  (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s})
Tactic: rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
A : Set Ω
hA : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} A
⊢ Eq (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
    (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
have a : levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω) = 0
Tactic: refine measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed ?_ hA ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
A : Set Ω
hA : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} A
a : levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω) = 0
⊢ Eq (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
    (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
have a₁ : ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed ?_ hA ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
A : Set Ω
hA : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} A
a : levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω) = 0
a₁ : ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
    (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) A : ℝ≥0∞)
have a₂ : ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed ?_ hA ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
hf : HasFiniteIntegral (ε := ℝ) (⇑f : (a : α) → ℝ) μ
⊢ Eq (α := ℝ) (∫ (ω : α), (f : (a : α) → ℝ) ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ (f : (a : α) → ℝ) a})
have rw : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
Tactic: rw [Integrable.integral_eq_integral_Ioc_meas_le (M := ‖f‖) ?_ f_nn ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
α : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
hf : HasFiniteIntegral (ε := ℝ) (⇑f : (a : α) → ℝ) μ
rw : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
⊢ Eq (α := ℝ) (∫ (ω : α), (f : (a : α) → ℝ) ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ (f : (a : α) → ℝ) a})
have rw₁ : (ae μ).EventuallyLE (β := ℝ) (⇑f : (a : α) → ℝ) fun (x : α) ↦ ‖f‖
Tactic: rw [Integrable.integral_eq_integral_Ioc_meas_le (M := ‖f‖) ?_ f_nn ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
⊢ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂μ ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
    μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
    ε * ‖f‖
Tactic: rw [BoundedContinuousFunction.integral_eq_integral_meas_le f μ f_nn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
t : ℝ
⊢ ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
    ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε
have h : ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
  (HAdd.hAdd (α := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (ENNReal.ofReal ε)).toReal
Tactic: convert!
      ENNReal.toReal_mono ?_ <|
        left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a})
          (f.continuous.measurable measurableSet_Ici)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
t : ℝ
h :
  ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
    (HAdd.hAdd (α := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
        (ENNReal.ofReal ε)).toReal
⊢ ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
    ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε
have left_measure_le_of_levyProkhorovEDist_lt : HAdd.hAdd (α := ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
    (ENNReal.ofReal ε) ≠
  ∞
Tactic: convert!
      ENNReal.toReal_mono ?_ <|
        left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a})
          (f.continuous.measurable measurableSet_Ici)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
t : ℝ
⊢ ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
    (HAdd.hAdd (α := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
        (ENNReal.ofReal ε)).toReal
have h : ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
  ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
    (ENNReal.ofReal ε).toReal
Tactic: rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
t : ℝ
h :
  ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
    ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      (ENNReal.ofReal ε).toReal
⊢ ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
    (HAdd.hAdd (α := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
        (ENNReal.ofReal ε)).toReal
have h₁ : ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
  ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε
Tactic: rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
have key : LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
  ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
Tactic: have key : (fun (t : ℝ) ↦ μ.real {a | t ≤ f a})
              ≤ (fun (t : ℝ) ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) := by
    intro t
    simp only [measureReal_def]
    convert!
      ENNReal.toReal_mono ?_ <|
        left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a})
          (f.continuous.measurable measurableSet_Ici)
    · rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]
    · exact ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
have f_mble : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) volume
Tactic: apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
f_mble :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
have f_bdd : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖), ‖μ.real {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}‖ ≤ μ.real univ
Tactic: apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) volume
have apply : Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}
Tactic: apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖), ‖μ.real {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}‖ ≤ μ.real univ
have apply : ∀ (t : ℝ), ‖μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}‖ ≤ μ.real univ
Tactic: apply Eventually.of_forall <| fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
t : ℝ
⊢ ‖μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}‖ ≤ μ.real univ
have simp : μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} ≤ μ.real univ
Tactic: simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
have intble₁ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
  (Ioc 0 ‖f‖) volume
Tactic: have intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) := by
    apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne
    · apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
      exact fun _ _ hst ↦ measure_mono (fun _ h ↦ hst.trans h)
    · apply Eventually.of_forall <| fun t ↦ ?_
      simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
      exact measureReal_mono (subset_univ _)