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'
h : ∀ a ∈ U, x (e a) = 0
x✝ : M'
⊢ (e.dualMap x ∘ₗ ↑e.symm) x✝ = x x✝
no goals