α : Type u
β : Type v
X : Type ?u.10931
ι : Type ?u.10934
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁
α : Type u
β : Type v
X : Type ?u.10931
ι : Type ?u.10934
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
rw [add_right_comm, dist_comm y₁]
no goals
α : Type u
β : Type v
X : Type ?u.10931
ι : Type ?u.10934
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁
apply dist_triangle4