awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
have pos : ∀ (LPμν_finite : levyProkhorovEDist μ ν = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
Tactic: by_cases LPμν_finite : levyProkhorovEDist μ ν = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
pos :
  ∀ (LPμν_finite : levyProkhorovEDist μ ν = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
have neg : ∀ (LPμν_finite : ¬levyProkhorovEDist μ ν = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
Tactic: by_cases LPμν_finite : levyProkhorovEDist μ ν = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
have pos : ∀ (LPνκ_finite : levyProkhorovEDist ν κ = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
Tactic: by_cases LPνκ_finite : levyProkhorovEDist ν κ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
pos :
  ∀ (LPνκ_finite : levyProkhorovEDist ν κ = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
have neg : ∀ (LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞), levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
Tactic: by_cases LPνκ_finite : levyProkhorovEDist ν κ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
have 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 ν κ) +
              ε
Tactic: apply levyProkhorovEDist_le_of_forall_add_pos_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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
⊢ (μ : (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 ν κ) +
        ε
have half_ε_pos : 0 < ε / 2
Tactic: have half_ε_pos : 0 < ε / 2 := ENNReal.div_pos ε_pos.ne' ofNat_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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
⊢ (μ : (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 ν κ) +
        ε
have lt_r : levyProkhorovEDist μ ν < r
Tactic: have lt_r : levyProkhorovEDist μ ν < r := lt_add_right LPμν_finite half_ε_pos.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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
⊢ (μ : (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 ν κ) +
        ε
have lt_s : levyProkhorovEDist ν κ < s
Tactic: have lt_s : levyProkhorovEDist ν κ < s := lt_add_right LPνκ_finite half_ε_pos.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ν κ + ε
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
have simp_rw₂ : levyProkhorovEDist ν κ + (ε / 2 + (levyProkhorovEDist μ ν + ε / 2)) =
  levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
Tactic: simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ν κ + ε)
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
have simp_rw₃ : levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + ε / 2 + ε / 2) =
  levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
Tactic: simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ν κ + ε)
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
have simp_rw₄ : levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + (ε / 2 + ε / 2)) =
  levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
Tactic: simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ν κ + ε)
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
have simp_rw₅ : levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + ε) = levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)
Tactic: simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ν κ + ε)
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
have simp_rw₆ : levyProkhorovEDist ν κ + levyProkhorovEDist μ ν + ε = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
Tactic: simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
      add_comm (levyProkhorovEDist μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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
⊢ (μ : (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 ν κ) +
        ε
have hs_add_r : 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 μ ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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
have ha : s ≠ ∞
Tactic: rw [← hs_add_r, ← ENNReal.toReal_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 ≠ ∞
⊢ s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
have hb : r ≠ ∞
Tactic: rw [← hs_add_r, ← ENNReal.toReal_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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 ν κ + ε
⊢ (μ : (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 ν κ) +
        ε
have hs_add_r' : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 (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 ν κ) +
        ε
have 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)
Tactic: rw [← hs_add_r', add_assoc, ← hs_add_r, add_assoc _ _ ε, ← hs_add_r]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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)
have neg : (μ : (a : Set Ω) → ℝ≥0∞) B ≤
  HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
have neg₁ : (κ : (a : Set Ω) → ℝ≥0∞) B ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 r.toReal B) : ℝ≥0∞) r ≤
    HAdd.hAdd (α := ℝ≥0∞) ((κ : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal (thickening r.toReal B)) : ℝ≥0∞) s + r
have 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
Tactic: grw [left_measure_le_of_levyProkhorovEDist_lt lt_s isOpen_thickening.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
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 + r.toReal) B) : ℝ≥0∞) (s + r)
have 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)
Tactic: grw [thickening_thickening_subset]