no goals
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
Φ : Submodule R (Module.Dual R M)
x : M
⊢ x ∈ dualCoannihilator Φ ↔ ∀ (φ : Module.Dual R M), φ ∈ Φ → ↑φ x = 0
simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]