no goals
α : Type ?u.81137
V : Type ?u.81140
P : Type ?u.81143
W : Type u_3
Q : Type u_1
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
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂)
rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
  inv_mul_cancel (dist_ne_zero.2 h), mul_one]