no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) =
    ‖p1 -ᵥ p2 + (r1 - r2) • v‖ * ‖p1 -ᵥ p2 + (r1 - r2) • v‖
rw [dist_eq_norm_vsub V (r1 • v +ᵥ p1), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul,
  add_comm, add_sub_assoc]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + abs (r1 - r2) * ‖v‖ * (abs (r1 - r2) * ‖v‖) =
    ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + abs (r1 - r2) * abs (r1 - r2) * ‖v‖ * ‖v‖
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + ‖(r1 - r2) • v‖ * ‖(r1 - r2) • v‖ =
    ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + abs (r1 - r2) * abs (r1 - r2) * ‖v‖ * ‖v‖
rw [norm_smul, Real.norm_eq_abs]
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + abs (r1 - r2) * ‖v‖ * (abs (r1 - r2) * ‖v‖) =
    ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + abs (r1 - r2) * abs (r1 - r2) * ‖v‖ * ‖v‖
ring
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + abs (r1 - r2) * abs (r1 - r2) * ‖v‖ * ‖v‖ =
    dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (‖v‖ * ‖v‖)
rw [dist_eq_norm_vsub V p1, abs_mul_abs_self, mul_assoc]