simp only [orthSpace, orthSpace', mem_map, mem_comap, Finsupp.toDualLin_coe, mem_dualAnnihilator,
  Finsupp.toDual_apply, Finsupp.total_apply, Finsupp.sum, smul_eq_mul]
α : 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)
inst✝ : Fintype η
⊢ x ∈ U.orthSpace ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 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)
inst✝ : Fintype η
⊢ (∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x) ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0