V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p1 p2 : P
hp1 : p1 ∈ s
⊢ inner (p1 -ᵥ ↑(↑(orthogonalProjection s) p2)) (↑(↑(orthogonalProjection s) p2) -ᵥ p2) = 0
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p1 p2 : P
hp1 : p1 ∈ s
⊢ dist p1 p2 * dist p1 p2 =
    dist p1 ↑(↑(orthogonalProjection s) p2) * dist p1 ↑(↑(orthogonalProjection s) p2) +
      dist p2 ↑(↑(orthogonalProjection s) p2) * dist p2 ↑(↑(orthogonalProjection s) p2)
rw [dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V _ p2,
  ← vsub_add_vsub_cancel p1 (orthogonalProjection s p2) p2,
  norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
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
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p1 p2 : P
hp1 : p1 ∈ s
⊢ inner (p1 -ᵥ ↑(↑(orthogonalProjection s) p2)) (↑(↑(orthogonalProjection s) p2) -ᵥ p2) = 0
exact Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p2 hp1)
  (orthogonalProjection_vsub_mem_direction_orthogonal s p2)