-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
dist : Dist.dist x z = Dist.dist (toGHSpace X) (toGHSpace Z)
dist₁ :
  hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
      (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) ≤
    hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
        (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
        (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))
dist₂ :
  hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
        (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
        (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) =
    hausdorffDist (α := GlueSpace hΦ hΨ) (toGlueL hΦ hΨ '' range (optimalGHInjl X Y))
        (toGlueL hΦ hΨ '' range (optimalGHInjr X Y)) +
      hausdorffDist (α := GlueSpace hΦ hΨ) (toGlueR hΦ hΨ '' range (optimalGHInjl Y Z))
        (toGlueR hΦ hΨ '' range (optimalGHInjr Y Z))
dist₃ :
  hausdorffDist (α := GlueSpace hΦ hΨ) (toGlueL hΦ hΨ '' range (optimalGHInjl X Y))
        (toGlueL hΦ hΨ '' range (optimalGHInjr X Y)) +
      hausdorffDist (α := GlueSpace hΦ hΨ) (toGlueR hΦ hΨ '' range (optimalGHInjl Y Z))
        (toGlueR hΦ hΨ '' range (optimalGHInjr Y Z)) =
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
      hausdorffDist (α := OptimalGHCoupling Y Z) (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z))
dist₄ :
  hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
      hausdorffDist (α := OptimalGHCoupling Y Z) (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) =
    Dist.dist (toGHSpace X) (toGHSpace Y) + Dist.dist (toGHSpace Y) (toGHSpace Z)
dist₅ : Dist.dist (toGHSpace X) (toGHSpace Y) + Dist.dist (toGHSpace Y) (toGHSpace Z) = Dist.dist x y + Dist.dist y z
⊢ Dist.dist x z ≤ Dist.dist x y + Dist.dist y z

Tactic:
calc
      dist x z = dist (toGHSpace X) (toGHSpace Z) := by
        rw [x.toGHSpace_rep, z.toGHSpace_rep]
      _ ≤ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
            (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) :=
        (ghDist_le_hausdorffDist ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y))
          ((toGlueR_isometry hΦ hΨ).comp (isometry_optimalGHInjr Y Z)))
      _ ≤ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
              (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
            hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
              (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) := by
        refine hausdorffDist_triangle <| hausdorffEDist_ne_top_of_nonempty_of_bounded
          (range_nonempty _) (range_nonempty _) ?_ ?_
        · exact (isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y)))).isBounded
        · exact (isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjr X Y)))).isBounded
      _ = hausdorffDist (toGlueL hΦ hΨ '' range (optimalGHInjl X Y))
              (toGlueL hΦ hΨ '' range (optimalGHInjr X Y)) +
            hausdorffDist (toGlueR hΦ hΨ '' range (optimalGHInjl Y Z))
              (toGlueR hΦ hΨ '' range (optimalGHInjr Y Z)) := by
        simp only [← range_comp, Comm]
      _ = hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
            hausdorffDist (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) := by
        rw [hausdorffDist_image (toGlueL_isometry hΦ hΨ),
          hausdorffDist_image (toGlueR_isometry hΦ hΨ)]
      _ = dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) := by
        rw [hausdorffDist_optimal, hausdorffDist_optimal, ghDist, ghDist]
      _ = dist x y + dist y z := by rw [x.toGHSpace_rep, y.toGHSpace_rep, z.toGHSpace_rep]

Premises used: Isometry.comp, GromovHausdorff.toGHSpace, Metric.hausdorffDist, GromovHausdorff.isometry_optimalGHInjr, Metric.toGlueL_isometry, Function.comp, GromovHausdorff.ghDist_le_hausdorffDist, GromovHausdorff.optimalGHInjl, Metric.toGlueL, Metric.toGlueR_isometry, Set.image, Dist.dist, Set.range, GromovHausdorff.optimalGHInjr, GromovHausdorff.isometry_optimalGHInjl, Metric.toGlueR