-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovEDist_triangle [OpensMeasurableSpace Ω] (μ ν κ : Measure Ω) :
    levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Proof state:
case hb
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 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:
exact ENNReal.add_ne_top.mpr ⟨LPμν_finite, half_ε_lt_top.ne⟩

Result:
no goals

Proof state:
case neg.h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
⊢ ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ⊤ →
        MeasurableSet B →
          μ B ≤
              κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε ∧
            κ B ≤
              μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε

Tactic:
intro ε B ε_pos ε_lt_top B_mble

Result:
case neg.h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Proof state:
case neg.h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (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 μ ν)]

Result:
case neg.h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Proof state:
case neg.h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Tactic:
have lt_r : levyProkhorovEDist μ ν < r := lt_add_right LPμν_finite half_ε_pos.ne'

Result:
case neg.h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Proof state:
case neg.h.refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 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
⊢ κ B ≤ μ (thickening (s.toReal + r.toReal) B) + (s + r)

Tactic:
calc κ B ≤ ν (thickening s.toReal B) + s :=
  right_measure_le_of_levyProkhorovEDist_lt lt_s B_mble
_ ≤ μ (thickening r.toReal (thickening s.toReal B)) + r + s :=
  add_le_add_right
    (right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet) s
_ = μ (thickening r.toReal (thickening s.toReal B)) + (s + r) := by rw [add_assoc, add_comm r]
_ ≤ μ (thickening (r.toReal + s.toReal) B) + (s + r) :=
  add_le_add_right (measure_mono (thickening_thickening_subset _ _ _)) _
_ = μ (thickening (s.toReal + r.toReal) B) + (s + r) := by rw [add_comm r.toReal]

Result:
no goals