no goals
α : Type ?u.64769
V : Type u_3
P : Type u_1
W : Type ?u.64778
Q : Type ?u.64781
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂
rw [midpoint_comm, dist_midpoint_left, dist_comm]