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

Proof state:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

Tactic:
convert ENNReal.toReal_mono ?_ <| levyProkhorovEDist_triangle μ ν κ

Result:
case h.e'_4
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤
⊢ levyProkhorovDist μ ν + levyProkhorovDist ν κ = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ).toReal

Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤
⊢ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ ≠ ⊤

Proof state:
case h.e'_4
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤
⊢ levyProkhorovDist μ ν + levyProkhorovDist ν κ = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ).toReal

Tactic:
simp only [levyProkhorovDist, ENNReal.toReal_add dμν_finite dνκ_finite]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤
⊢ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ ≠ ⊤

Tactic:
exact ENNReal.add_ne_top.mpr ⟨dμν_finite, dνκ_finite⟩

Result:
no goals

Proof state:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

Tactic:
have dνκ_finite := (levyProkhorovEDist_lt_top ν κ).ne

Result:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

Proof state:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

Tactic:
have dμν_finite := (levyProkhorovEDist_lt_top μ ν).ne

Result:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ⊤
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ