∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x_2 : Y) (y : X), Metric.glueDist Φ Ψ ε (Sum.inr x_2) (Sum.inl y) = (⨅ p, dist y (Φ p) + dist x_2 (Ψ p)) + ε