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 Ω
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
⊢ ENNReal.ofReal δ < ENNReal.ofReal ε.toReal

Tactic:
simpa [ofReal_toReal_eq_iff.mpr ε_lt_top.ne] using ε_gt

Premises used: Iff.mpr, ENNReal.ofReal_toReal_eq_iff, 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
⊢ δ < ε.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
-- 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
ε_gt' : δ < ε.toReal
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) (ENNReal.ofReal ε.toReal)

Tactic:
h ε.toReal B ε_gt' B_mble

Premises used: 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 ν
δ : ℝ
δ_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
h₁ : ε = ENNReal.ofReal ε.toReal
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
convert! h ε.toReal B ε_gt' B_mble

Premises used: 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 ν
δ : ℝ
δ_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
⊢ ε = ENNReal.ofReal ε.toReal

Tactic:
(ENNReal.ofReal_toReal ε_lt_top.ne).symm

Premises used: ENNReal.ofReal_toReal, Eq.symm, 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
ε_gt' : δ < ε.toReal
⊢ ε = ENNReal.ofReal ε.toReal

Tactic:
exact (ENNReal.ofReal_toReal ε_lt_top.ne).symm

Premises used: ENNReal.ofReal_toReal, Eq.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
α : Type u_2
x x_1 : LevyProkhorov α
μ ν : α
⊢ (ofMeasure μ).toMeasure = (ofMeasure ν).toMeasure → ofMeasure μ = ofMeasure ν

Tactic:
congr!
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : LevyProkhorov (FiniteMeasure Ω)
⊢ levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω) =
    ENNReal.ofReal (levyProkhorovDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω))

Tactic:
simp [levyProkhorovDist, levyProkhorovEDist_ne_top]

Premises used: MeasureTheory.levyProkhorovEDist_ne_top, MeasureTheory.levyProkhorovDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : LevyProkhorov (Measure Ω)
⊢ edist μ ν = levyProkhorovEDist μ.toMeasure ν.toMeasure

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : LevyProkhorov (FiniteMeasure Ω)
⊢ edist μ ν = levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : LevyProkhorov (FiniteMeasure Ω)
⊢ dist μ ν = levyProkhorovDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
⊢ edist μ ν = levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)

Tactic:
rfl

Premises used: MeasureTheory.ProbabilityMeasure, MeasureTheory.ProbabilityMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
⊢ dist μ ν = levyProkhorovDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)

Tactic:
rfl

Premises used: MeasureTheory.ProbabilityMeasure, MeasureTheory.ProbabilityMeasure.toMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
a : μ.toMeasure = ν.toMeasure
⊢ μ = ν

Tactic:
apply toMeasure_injective

Premises used: MeasureTheory.LevyProkhorov.toMeasure_injective
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
a : (↑μ.toMeasure : Measure Ω) = (↑ν.toMeasure : Measure Ω)
⊢ μ.toMeasure = ν.toMeasure

Tactic:
apply ProbabilityMeasure.toMeasure_injective

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure_injective
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ Eq (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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}
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∞)
⊢ (↑μ.toMeasure : Measure Ω) = (↑ν.toMeasure : Measure Ω)

Tactic:
refine ext_of_generate_finite _ ?_ isPiSystem_isClosed (fun A hA ↦ ?_) (by simp)

Premises used: MeasureTheory.ext_of_generate_finite, isPiSystem_isClosed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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}
a₁ a₂ :
  Eq.{u_1 + 1} (α := MeasurableSpace Ω)
    (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s})
    (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s})
⊢ inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}

Tactic:
rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]

Premises used: borel_eq_generateFrom_isClosed, BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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∞)

Tactic:
measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed ?_ hA ?_ ?_

Premises used: MeasureTheory.measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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∞)
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∞)

Tactic:
refine measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed ?_ hA ?_ ?_

Premises used: MeasureTheory.measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ levyProkhorovEDist (↑μ.toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω) = 0

Tactic:
simpa [dist_probabilityMeasure_def, levyProkhorovDist, toReal_eq_zero_iff] using h

Premises used: MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def, MeasureTheory.levyProkhorovDist, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨1, Real.zero_lt_one, measure_ne_top _ _⟩

Premises used: MeasureTheory.measure_ne_top, Real.zero_lt_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑μ.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨1, Real.zero_lt_one, measure_ne_top _ _⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨1, Real.zero_lt_one, measure_ne_top _ _⟩

Premises used: MeasureTheory.measure_ne_top, Real.zero_lt_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ ∃ δ > 0, Ne (α := ℝ≥0∞) (((↑ν.toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ A) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨1, Real.zero_lt_one, measure_ne_top _ _⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : α) → ℝ) μ
rw₁ : (ae μ).EventuallyLE (β := ℝ) (⇑f : (a : α) → ℝ) fun (x : α) ↦ ‖f‖
⊢ Eq (α := ℝ) (∫ (ω : α), (f : (a : α) → ℝ) ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ (f : (a : α) → ℝ) a})

Tactic:
rw [Integrable.integral_eq_integral_Ioc_meas_le (M := ‖f‖) ?_ f_nn ?_]

Premises used: MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : α) → ℝ) μ
⊢ Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ

Tactic:
⟨f.continuous.measurable.aestronglyMeasurable, hf⟩

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable, BoundedContinuousFunction.continuous, And.intro, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : α) → ℝ) μ
⊢ Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ

Tactic:
exact ⟨f.continuous.measurable.aestronglyMeasurable, hf⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : α) → ℝ) μ
⊢ (ae μ).EventuallyLE (β := ℝ) (⇑f : (a : α) → ℝ) fun (x : α) ↦ ‖f‖

Tactic:
Eventually.of_forall (fun x ↦ BoundedContinuousFunction.apply_le_norm f x)

Premises used: Filter.Eventually.of_forall, BoundedContinuousFunction.apply_le_norm, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : α) → ℝ) μ
⊢ (ae μ).EventuallyLE (β := ℝ) (⇑f : (a : α) → ℝ) fun (x : α) ↦ ‖f‖

Tactic:
exact Eventually.of_forall (fun x ↦ BoundedContinuousFunction.apply_le_norm f x)

Premises used: Filter.Eventually.of_forall, BoundedContinuousFunction.apply_le_norm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
α : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
inst_3 : IsFiniteMeasure μ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
⊢ Eq (α := ℝ) (∫ (ω : α), (f : (a : α) → ℝ) ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ (f : (a : α) → ℝ) a})

Tactic:
integral_eq_integral_meas_le_of_hasFiniteIntegral _ _ f_nn (f.integrable μ).2

Premises used: BoundedContinuousFunction.integrable, And.right, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : Ω) → ℝ)
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‖
⊢ ∫ (ω : Ω), (f : (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]

Premises used: MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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}) ≤
    (HAdd.hAdd (α := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
        (ENNReal.ofReal ε)).toReal

Tactic:
ENNReal.toReal_mono ?_ <|
        left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a})
          (f.continuous.measurable measurableSet_Ici)

Premises used: BoundedContinuousFunction.continuous, Continuous.measurable, MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt, measurableSet_Ici, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
left_measure_le_of_levyProkhorovEDist_lt :
  HAdd.hAdd (α := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (ENNReal.ofReal ε) ≠
    ∞
⊢ ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
    ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε

Tactic:
convert!
      ENNReal.toReal_mono ?_ <|
        left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a})
          (f.continuous.measurable measurableSet_Ici)

Premises used: BoundedContinuousFunction.continuous, Continuous.measurable, MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt, measurableSet_Ici, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
h₁ h₂ :
  ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε =
    ENNReal.toReal ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) + ε
⊢ 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:
rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]

Premises used: ENNReal.toReal_add, MeasureTheory.measure_ne_top, LT.lt.le, ENNReal.toReal_ofReal, ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : ℝ
⊢ HAdd.hAdd (α := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (ENNReal.ofReal ε) ≠
    ∞

Tactic:
ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, And.intro, ENNReal.ofReal_ne_top, ENNReal.add_ne_top