simp_rw [orthSpace, mem_map, mem_orthSpace'_iff]
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
U : Submodule R (ι → R)
w : ι → R
⊢ w ∈ U.orthSpace ↔ ∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ y, (∀ x ∈ U, (Finsupp.total ι R R x) y = 0) ∧ Finsupp.lcoeFun y = w) ↔
    ∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0