awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ENNReal.toReal_pos hε₀.ne' hε_top.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν = levyProkhorovEDist ν μ

Tactic:
simp only [levyProkhorovEDist, and_comm]

Premises used: and_comm, MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
pos :
  ∀ (LPμν_finite : levyProkhorovEDist μ ν = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
neg :
  ∀ (LPμν_finite : ¬levyProkhorovEDist μ ν = ∞),
    levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Tactic:
by_cases LPμν_finite : levyProkhorovEDist μ ν = ∞

Premises used: MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : levyProkhorovEDist μ ν = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Tactic:
simp [LPμν_finite]
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
pos :
  ∀ (LPνκ_finite : levyProkhorovEDist ν κ = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
neg :
  ∀ (LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞),
    levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Tactic:
by_cases LPνκ_finite : levyProkhorovEDist ν κ = ∞

Premises used: MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : levyProkhorovEDist ν κ = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Tactic:
simp [LPνκ_finite]
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
neg :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞)
                  ((κ : (a : Set Ω) → ℝ≥0∞)
                      (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) :
                    ℝ≥0∞)
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε ∧
            (κ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞)
                  ((μ : (a : Set Ω) → ℝ≥0∞)
                      (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) :
                    ℝ≥0∞)
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + 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 Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
⊢ 0 < ε / 2

Tactic:
have half_ε_pos : 0 < ε / 2 := ENNReal.div_pos ε_pos.ne' ofNat_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
⊢ levyProkhorovEDist μ ν < r

Tactic:
have lt_r : levyProkhorovEDist μ ν < r := lt_add_right LPμν_finite half_ε_pos.ne'
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
⊢ levyProkhorovEDist ν κ < s

Tactic:
have lt_s : levyProkhorovEDist ν κ < s := lt_add_right LPνκ_finite half_ε_pos.ne'
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
simp_rw : levyProkhorovEDist ν κ + ε / 2 + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
simp_rw₁ :
  levyProkhorovEDist ν κ + ε / 2 + (levyProkhorovEDist μ ν + ε / 2) =
    levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
simp_rw₂ :
  levyProkhorovEDist ν κ + (ε / 2 + (levyProkhorovEDist μ ν + ε / 2)) =
    levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
simp_rw₃ :
  levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + ε / 2 + ε / 2) =
    levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
simp_rw₄ :
  levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + (ε / 2 + ε / 2)) =
    levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
simp_rw₅ : levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + ε) = levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
simp_rw₆ : levyProkhorovEDist ν κ + levyProkhorovEDist μ ν + ε = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε

Tactic:
simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]

Premises used: add_assoc, HDiv.hDiv, add_comm, ENNReal.add_halves, OfNat.ofNat, MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε

Tactic:
have hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε := by
    simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
ha : s ≠ ∞
hb : r ≠ ∞
⊢ s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal

Tactic:
rw [← hs_add_r, ← ENNReal.toReal_add]

Premises used: ENNReal.toReal_add
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ r ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal

Tactic:
have hs_add_r' : s.toReal + r.toReal
      = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal := by
    rw [← hs_add_r, ← ENNReal.toReal_add]
    · finiteness
    · finiteness
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
neg :
  (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r) ∧
    (κ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞)
          ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) : ℝ≥0∞)
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    (κ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) : ℝ≥0∞)
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Tactic:
rw [← hs_add_r', add_assoc, ← hs_add_r, add_assoc _ _ ε, ← hs_add_r]

Premises used: add_assoc
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r) ∧
    (κ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
neg :
  (μ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
neg₁ :
  (κ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r) ∧
    (κ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal B) : ℝ≥0∞) r

Tactic:
left_measure_le_of_levyProkhorovEDist_lt lt_r B_mble

Premises used: MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
grw grw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) s + r ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) s + r
⊢ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal B) : ℝ≥0∞) r ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) s + r

Tactic:
grw [left_measure_le_of_levyProkhorovEDist_lt lt_s isOpen_thickening.measurableSet]

Premises used: Metric.isOpen_thickening, IsOpen.measurableSet, MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) s + r =
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) (s + r)

Tactic:
add_assoc _ _ _

Premises used: add_assoc
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
grw grw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) (s + r) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
grw [thickening_thickening_subset]

Premises used: Metric.thickening_thickening_subset
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
calc :
  HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal B) : ℝ≥0∞) r ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) s + r
calc₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) (s + r) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
calc μ B ≤ ν (thickening r.toReal B) + r :=
      left_measure_le_of_levyProkhorovEDist_lt lt_r B_mble
    _ ≤ κ (thickening s.toReal (thickening r.toReal B)) + s + r := by
      grw [left_measure_le_of_levyProkhorovEDist_lt lt_s isOpen_thickening.measurableSet]
    _ = κ (thickening s.toReal (thickening r.toReal B)) + (s + r) := add_assoc _ _ _
    _ ≤ κ (thickening (s.toReal + r.toReal) B) + (s + r) := by grw [thickening_thickening_subset]

Premises used: add_assoc, Metric.thickening, ENNReal.toReal, HAdd.hAdd, MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ (κ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal B) : ℝ≥0∞) s

Tactic:
right_measure_le_of_levyProkhorovEDist_lt lt_s B_mble

Premises used: MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
grw grw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) r + s ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) r + s
⊢ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal B) : ℝ≥0∞) s ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) r + s

Tactic:
grw [right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet]

Premises used: Metric.isOpen_thickening, IsOpen.measurableSet, MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt