n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ dist n k ≤ dist n m + dist m k
n m k : ℕ
⊢ dist n k ≤ dist n m + dist m k
have : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n)) := by
  simp [dist.def, add_comm, add_left_comm, add_assoc]
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ n - k + (k - n) ≤ n - m + (m - k) + (k - m + (m - n))
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ dist n k ≤ dist n m + dist m k
rw [this, dist.def]
no goals
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ n - k + (k - n) ≤ n - m + (m - k) + (k - m + (m - n))
exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub
no goals
n m k : ℕ
⊢ dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
simp [dist.def, add_comm, add_left_comm, add_assoc]