case hv
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 }
p : P
⊢ p -ᵥ ↑(↑(orthogonalProjection s) p) ∈ (direction s)ᗮ
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 }
p : P
⊢ ↑(_root_.orthogonalProjection (direction s)) (p -ᵥ ↑(↑(orthogonalProjection s) p)) = 0
apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
case hv
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 }
p : P
c : V
hc : c ∈ direction s
⊢ inner c (p -ᵥ ↑(↑(orthogonalProjection s) p)) = 0
case hv
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 }
p : P
⊢ p -ᵥ ↑(↑(orthogonalProjection s) p) ∈ (direction s)ᗮ
intro c hc
no goals
case hv
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 }
p : P
c : V
hc : c ∈ direction s
⊢ inner c (p -ᵥ ↑(↑(orthogonalProjection s) p)) = 0
rw [← neg_vsub_eq_vsub_rev, inner_neg_right,
  orthogonalProjection_vsub_mem_direction_orthogonal s p c hc, neg_zero]