ι : Type ?u.46254
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y z : E
h : SameRay ℝ (y - x) (z - y)
⊢ ‖x - y‖ + ‖y - z‖ = ‖x - z‖
ι : Type ?u.46254
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y z : E
h : y ∈ [x-[ℝ]z]
⊢ dist x y + dist y z = dist x z
simp only [dist_eq_norm, mem_segment_iff_sameRay] at *
no goals
ι : Type ?u.46254
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y z : E
h : SameRay ℝ (y - x) (z - y)
⊢ ‖x - y‖ + ‖y - z‖ = ‖x - z‖
simpa only [sub_add_sub_cancel', norm_sub_rev] using h.norm_add.symm