no goals
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 : P
⊢ dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 p2)
rw [dist_left_midpoint (𝕜 := ℝ) p1 p2, dist_right_midpoint (𝕜 := ℝ) p1 p2]