no goals
α : Type ?u.48468
V : Type u_2
P : Type u_1
W : Type ?u.48477
Q : Type ?u.48480
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist (↑(homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
rw [homothety_eq_lineMap, dist_lineMap_right]