simp_rw [mem_relOrthSpace_iff, mem_subtypeFunEquiv_iff, mem_orthSpace_iff'']
case h
α : 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 K (↑s → K)
x : ι → K
⊢ x ∈ s.relOrthSpace ↑((s.subtypeFunEquiv K) U) ↔ x ∈ ↑((s.subtypeFunEquiv K) U.orthSpace)
case h
α : 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 K (↑s → K)
x : ι → K
⊢ (∃ l, ⇑↑l = x ∧ ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0) ↔
    support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0