case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h : ↑(↑(orthogonalProjection K) v) = v
⊢ v ∈ K

case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h : v ∈ K
⊢ ∀ (w : E), w ∈ K → inner (v - v) w = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ ↑(↑(orthogonalProjection K) v) = v ↔ v ∈ K
refine' ⟨fun h => _, fun h => eq_orthogonalProjection_of_mem_of_inner_eq_zero h _⟩
case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h : ↑(↑(orthogonalProjection K) v) = v
⊢ ↑(↑(orthogonalProjection K) v) ∈ K
case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h : ↑(↑(orthogonalProjection K) v) = v
⊢ v ∈ K
rw [← h]
no goals
case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h : ↑(↑(orthogonalProjection K) v) = v
⊢ ↑(↑(orthogonalProjection K) v) ∈ K
simp
no goals
case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.516714
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h : v ∈ K
⊢ ∀ (w : E), w ∈ K → inner (v - v) w = 0
simp