no goals
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∀ (φ : Module.Dual K V), φ ∈ dualAnnihilator W → ↑φ v = 0) ↔ v ∈ W
rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]