awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
ε_top : ¬ε₂ = ∞
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞)

Tactic:
measure_mono (μ := ν) (thickening_mono (toReal_mono ε_top h_le) B)

Premises used: Metric.thickening_mono, MeasureTheory.measure_mono, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
ε_top : ¬ε₂ = ∞
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞)

Tactic:
exact measure_mono (μ := ν) (thickening_mono (toReal_mono ε_top h_le) B)

Premises used: Metric.thickening_mono, MeasureTheory.measure_mono, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
obtain :
  ∀ (c' : ℝ≥0∞)
    (hc' :
      Membership.mem (γ := Set ℝ≥0∞)
        {ε : ℝ≥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∞) ε}
        c')
    (lt_c : c' < c),
    (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c

Tactic:
obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h

Premises used: sInf_lt_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  Membership.mem (γ := Set ℝ≥0∞)
    {ε : ℝ≥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∞) ε}
    c'
lt_c : c' < c
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c

Tactic:
meas_le_of_le_of_forall_le_meas_thickening_add μ ν lt_c.le (hc' B B_mble).1

Premises used: LT.lt.le, And.left, MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  Membership.mem (γ := Set ℝ≥0∞)
    {ε : ℝ≥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∞) ε}
    c'
lt_c : c' < c
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c

Tactic:
exact meas_le_of_le_of_forall_le_meas_thickening_add μ ν lt_c.le (hc' B B_mble).1

Premises used: LT.lt.le, And.left, MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
obtain :
  ∀ (c' : ℝ≥0∞)
    (hc' :
      Membership.mem (γ := Set ℝ≥0∞)
        {ε : ℝ≥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∞) ε}
        c')
    (lt_c : c' < c),
    (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c

Tactic:
obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h

Premises used: sInf_lt_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  Membership.mem (γ := Set ℝ≥0∞)
    {ε : ℝ≥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∞) ε}
    c'
lt_c : c' < c
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c

Tactic:
meas_le_of_le_of_forall_le_meas_thickening_add ν μ lt_c.le (hc' B B_mble).2

Premises used: LT.lt.le, And.right, MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  Membership.mem (γ := Set ℝ≥0∞)
    {ε : ℝ≥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∞) ε}
    c'
lt_c : c' < c
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c

Tactic:
exact meas_le_of_le_of_forall_le_meas_thickening_add ν μ lt_c.le (hc' B B_mble).2

Premises used: LT.lt.le, And.right, MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
h₁ : ∀ (ε : ℝ≥0), 0 < ε → δ < ∞ → levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h₁ : δ < ∞ → levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
⊢ δ < ∞ → levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
pos : ∀ (ε_top : (↑ε : ℝ≥0∞) = ∞), levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
neg : ∀ (ε_top : ¬(↑ε : ℝ≥0∞) = ∞), levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
⊢ levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)

Tactic:
by_cases ε_top : ε = ∞
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
ε_top : (↑ε : ℝ≥0∞) = ∞
⊢ levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)

Tactic:
simp only [ε_top, add_top, le_top]

Premises used: add_top, le_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
ε_top : ¬(↑ε : ℝ≥0∞) = ∞
neg :
  Membership.mem (γ := Set ℝ≥0∞)
    {ε : ℝ≥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∞) ε}
    (δ + (↑ε : ℝ≥0∞))
⊢ levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)

Tactic:
apply sInf_le

Premises used: sInf_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
ε_top : ¬(↑ε : ℝ≥0∞) = ∞
B : Set Ω
B_mble : MeasurableSet B
⊢ 0 < (↑ε : ℝ≥0∞)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        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∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
ε_top : ¬(↑ε : ℝ≥0∞) = ∞
B : Set Ω
B_mble : MeasurableSet B
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + (↑ε : ℝ≥0∞)).toReal B) : ℝ≥0∞)
        (δ + (↑ε : ℝ≥0∞)) ∧
    (ν : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + (↑ε : ℝ≥0∞)).toReal B) : ℝ≥0∞) (δ + (↑ε : ℝ≥0∞))

Tactic:
simpa only [add_assoc] using h ε B (by positivity) coe_lt_top B_mble

Premises used: ENNReal.ofNNReal, add_assoc, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥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∞) ε
pos : ∀ (δ_top : δ = ∞), levyProkhorovEDist μ ν ≤ δ
neg : ∀ (δ_top : ¬δ = ∞), levyProkhorovEDist μ ν ≤ δ
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
by_cases δ_top : δ = ∞
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥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∞) ε
δ_top : δ = ∞
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
simp only [δ_top, le_top]

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥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∞) ε
δ_top : ¬δ = ∞
neg :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
apply levyProkhorovEDist_le_of_forall_add_pos_le

Premises used: MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥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∞) ε
δ_top : ¬δ = ∞
x : ℝ≥0∞
B : Set Ω
x_pos : 0 < x
x_lt_top : x < ∞
B_mble : MeasurableSet B
⊢ δ + x < ∞

Tactic:
simp only [add_lt_top, Ne.lt_top δ_top, x_lt_top, and_self]

Premises used: and_self, Ne.lt_top, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥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∞) ε
δ_top : ¬δ = ∞
x : ℝ≥0∞
B : Set Ω
x_pos : 0 < x
x_lt_top : x < ∞
B_mble : MeasurableSet B
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + x).toReal B) : ℝ≥0∞) δ + x ∧
    (ν : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + x).toReal B) : ℝ≥0∞) δ + x

Tactic:
simpa only [← add_assoc] using h (δ + x) B (ENNReal.lt_add_right δ_top x_pos.ne.symm)
    (by simp only [add_lt_top, Ne.lt_top δ_top, x_lt_top, and_self]) B_mble

Premises used: ENNReal.lt_add_right, add_assoc, Ne.symm, HAdd.hAdd, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν ≤ max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ)

Tactic:
sInf_le fun B _ ↦ ⟨?_, ?_⟩

Premises used: sInf_le, And.intro, MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
refine_1 :
  ∀ (B : Set Ω),
    MeasurableSet B →
      (μ : (a : Set Ω) → ℝ≥0∞) B ≤
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((ν : (a : Set Ω) → ℝ≥0∞)
              (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
            ℝ≥0∞)
          (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
refine_2 :
  ∀ (B : Set Ω),
    MeasurableSet B →
      (ν : (a : Set Ω) → ℝ≥0∞) B ≤
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞)
              (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
            ℝ≥0∞)
          (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
⊢ levyProkhorovEDist μ ν ≤ max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ)

Tactic:
refine sInf_le fun B _ ↦ ⟨?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
B : Set Ω
h : MeasurableSet B
refine_1 :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) B : ℝ≥0∞)
    (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞)
          (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
        ℝ≥0∞)
      (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)

Tactic:
apply le_add_left

Premises used: le_add_left
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
B : Set Ω
h : MeasurableSet B
refine_2 :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) B : ℝ≥0∞)
    (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞)
          (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
        ℝ≥0∞)
      (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)

Tactic:
apply le_add_left

Premises used: le_add_left
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
B : Set Ω
h : MeasurableSet B
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) B : ℝ≥0∞)
    (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)

Tactic:
simp [measure_mono]

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
B : Set Ω
h : MeasurableSet B
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) B : ℝ≥0∞)
    (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)

Tactic:
simp [measure_mono]

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [measure_lt_top]

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
⊢ levyProkhorovEDist μ ν ≠ ∞

Tactic:
(levyProkhorovEDist_lt_top μ ν).ne

Premises used: MeasureTheory.levyProkhorovEDist_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
rw : levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ∞)
⊢ levyProkhorovEDist μ μ = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← csInf_Ioo zero_lt_top]

Premises used: ENNReal.zero_lt_top, csInf_Ioo, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ∞)

Tactic:
sInf_le_sInf fun ε ⟨hε₀, hε_top⟩ B _ ↦ and_self_iff.2 ?_

Premises used: Iff.mpr, sInf_le_sInf, LE.le, Metric.thickening, And, ENNReal.toReal, HAdd.hAdd, _private.0.MeasureTheory.levyProkhorovEDist_self.match_1, and_self_iff, DFunLike.coe, MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
refine :
  ∀ (ε : ℝ≥0∞),
    Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) ε →
      ∀ (B : Set Ω),
        MeasurableSet B →
          ∀ (hε₀ : 0 < ε) (hε_top : ε < ∞),
            (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ∞)

Tactic:
refine sInf_le_sInf fun ε ⟨hε₀, hε_top⟩ B _ ↦ and_self_iff.2 ?_
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) ε
B : Set Ω
h_1 : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ∞
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
le_add_right <| measure_mono <| self_subset_thickening ?_ _

Premises used: Metric.self_subset_thickening, MeasureTheory.measure_mono, le_add_right
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) ε
B : Set Ω
h_1 : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ∞
refine : 0 < ε.toReal
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε

Tactic:
refine le_add_right <| measure_mono <| self_subset_thickening ?_ _

Premises used: Metric.self_subset_thickening, MeasureTheory.measure_mono, le_add_right
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) ε
B : Set Ω
h_1 : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ∞
⊢ 0 < ε.toReal

Tactic:
ENNReal.toReal_pos hε₀.ne' hε_top.ne

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