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 : 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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
have f_mble : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (t : ℝ) ↦ ν.real (thickening ε {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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
f_mble :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
have f_bdd : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖),
  ‖ν.real (thickening ε {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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) volume
have apply : Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖),
    ‖ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})‖ ≤ ν.real univ
have apply : ∀ (t : ℝ), ‖ν.real (thickening ε {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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
t : ℝ
⊢ ‖ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})‖ ≤ ν.real univ
have simp : ν.real (thickening ε {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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ (@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 (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
Tactic: have intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {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 <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)
    · apply Eventually.of_forall <| fun t ↦ ?_
      simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
      exact ENNReal.toReal_mono (by finiteness) <| measure_mono (subset_univ _)
-- 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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
⊢ (@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 apply : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
    ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
    ε * ‖f‖
Tactic: apply le_trans (setIntegral_mono (s := Ioc 0 ‖f‖) ?_ ?_ key)
-- 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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
apply :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
      ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
apply₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ (@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 apply₂ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε) (Ioc 0 ‖f‖) volume
Tactic: apply le_trans (setIntegral_mono (s := Ioc 0 ‖f‖) ?_ ?_ key)
-- 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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
      ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
have rw : HAdd.hAdd (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦
      ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦ ε) ≤
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
    ε * ‖f‖
Tactic: rw [integral_add]
-- 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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
rw :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦
        ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦ ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
      ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
have hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
  (fun (x : ℝ) ↦ ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})) (Measure.restrict volume (Ioc 0 ‖f‖))
Tactic: rw [integral_add]
-- 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}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
rw :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦
        ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦ ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
hf :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})) (Measure.restrict volume (Ioc 0 ‖f‖))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
      ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
have hg : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ ε) (Measure.restrict volume (Ioc 0 ‖f‖))
Tactic: rw [integral_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    (𝓝[>] 0)
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
have hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0,
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
    (Measure.restrict volume A)
Tactic: apply tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A)
        (F := fun ε t ↦ (μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
hF_meas :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
      (Measure.restrict volume A)
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    (𝓝[>] 0)
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
have h_bound : ∀ᶠ (n : ℝ) in 𝓝[>] 0,
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
Tactic: apply tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A)
        (F := fun ε t ↦ (μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
hF_meas :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
      (Measure.restrict volume A)
h_bound :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
      ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    (𝓝[>] 0)
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
have bound_integrable : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace 1 (Measure.restrict volume A)
Tactic: apply tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A)
        (F := fun ε t ↦ (μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
hF_meas :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
      (Measure.restrict volume A)
h_bound :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
      ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
bound_integrable : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace 1 (Measure.restrict volume A)
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    (𝓝[>] 0)
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
have h_lim : ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
  Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)) (𝓝[>] 0)
    (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}) : ℝ))
Tactic: apply tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A)
        (F := fun ε t ↦ (μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
      (Measure.restrict volume A)
have apply : ∀ (n : ℝ),
  Measurable (β := ℝ) fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)
Tactic: apply Eventually.of_forall fun n ↦ Measurable.aestronglyMeasurable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
n : ℝ
⊢ Measurable (β := ℝ) fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)
have simp : Measurable (β := ℝ≥0) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})
Tactic: simp only [measurable_coe_nnreal_real_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
n : ℝ
⊢ Measurable (β := ℝ≥0) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})
have apply : ∀ (s t : ℝ) (hst : s ≤ t),
  LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | s ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
Tactic: apply measurable_toNNReal.comp <| Antitone.measurable (fun s t hst ↦ ?_)