case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ Kᗮᗮ ↔ v ∈ K
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
⊢ Kᗮᗮ = K
ext v
case h.mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ Kᗮᗮ → v ∈ K

case h.mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ K → v ∈ Kᗮᗮ
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ Kᗮᗮ ↔ v ∈ K
constructor
case h.mp.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
⊢ y + z ∈ Kᗮᗮ → y + z ∈ K
case h.mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ Kᗮᗮ → v ∈ K
obtain ⟨y, hy, z, hz, rfl⟩ := K.exists_sum_mem_mem_orthogonal v
case h.mp.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ y + z ∈ K
case h.mp.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
⊢ y + z ∈ Kᗮᗮ → y + z ∈ K
intro hv
case h.mp.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hz' : z = 0
⊢ y + z ∈ K
case h.mp.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ y + z ∈ K
have hz' : z = 0 := by
  have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
  simpa [inner_add_right, hyz] using hv z hz
no goals
case h.mp.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hz' : z = 0
⊢ y + z ∈ K
simp [hy, hz']
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hyz : inner z y = 0
⊢ z = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ z = 0
have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hyz : inner z y = 0
⊢ z = 0
simpa [inner_add_right, hyz] using hv z hz
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ inner z y = 0
simp [hz y hy, inner_eq_zero_symm]
case h.mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ inner w v = 0
case h.mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ K → v ∈ Kᗮᗮ
intro hv w hw
case h.mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ inner v w = 0
case h.mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ inner w v = 0
rw [inner_eq_zero_symm]
no goals
case h.mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.776857
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ inner v w = 0
exact hw v hv