α : Type u
β : Type v
X : Type ?u.10546
ι : Type ?u.10549
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.10546
ι : Type ?u.10549
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
rw [add_left_comm, dist_comm x₁, ← add_assoc]
no goals
α : Type u
β : Type v
X : Type ?u.10546
ι : Type ?u.10549
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂
apply dist_triangle4