𝕜 : Type u_2
E : Type u_1
F : Type ?u.34324
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 (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u (x - y) = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.34324
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 (↑v) x = inner (↑v) y
⊢ x - y ∈ Kᗮ
intro u hu
𝕜 : Type u_2
E : Type u_1
F : Type ?u.34324
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 (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u x = inner u y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.34324
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 (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u (x - y) = 0
rw [inner_sub_right, sub_eq_zero]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.34324
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 (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u x = inner u y
exact h ⟨u, hu⟩