rw [relOrthSpace, mem_inf, mem_orthSpace_iff'', mem_supportedFun_iff]
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ w ∈ s.relOrthSpace U ↔ ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s ↔
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0