𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ ∀ (u : E), u ∈ K → inner (x - y) u = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ x - y ∈ Kᗮ
rw [mem_orthogonal']
𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner (x - y) u = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ ∀ (u : E), u ∈ K → inner (x - y) u = 0
intro u hu
𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner x u = inner y u
𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner (x - y) u = 0
rw [inner_sub_left, sub_eq_zero]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.32170
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner x u = inner y u
exact h ⟨u, hu⟩