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

Proof state:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

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

Result:
case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : levyProkhorovEDist ν κ = ⊤
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
⊢ levyProkhorovEDist μ κ ≤ 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
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Tactic:
have half_ε_lt_top : ε / 2 < ∞ := ENNReal.div_lt_top ε_lt_top.ne two_ne_zero

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 < ⊤
⊢ μ 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
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Tactic:
let s := levyProkhorovEDist ν κ + ε / 2

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
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Proof state:
Ω : 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
⊢ μ (thickening r.toReal (thickening s.toReal B)) + r + s = μ (thickening r.toReal (thickening s.toReal B)) + (s + r)

Tactic:
rw [add_assoc, add_comm r]

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 Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Tactic:
have half_ε_pos : 0 < ε / 2 := ENNReal.div_pos ε_pos.ne' ofNat_ne_top

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
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε