no goals
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
⊢ Sum.dist p q = glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 p q
cases p <;> cases q <;> first |rfl|simp [Sum.dist, glueDist, dist_comm, add_comm,
  add_left_comm, add_assoc]
no goals
case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inr val✝)
rfl
no goals
case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inl val✝)
simp [Sum.dist, glueDist, dist_comm, add_comm,
add_left_comm, add_assoc]