no goals
α✝ : Type u
β : Type v
X : Type ?u.3732
ι : Type ?u.3735
α : Sort u_1
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
⊢ dist x y + dist y x = 2 * dist x y
rw [two_mul, dist_comm]