refine ⟨fun h ↦ ⟨e.dualMap x, h, by ext; simp⟩, ?_⟩
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∀ a ∈ U, x (e a) = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x) → ∀ a ∈ U, x (e a) = 0