no goals
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : M →ₗ[R] N
⊢ ↑(dualTensorHom R M N) (↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b)) x) = x
rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.apply_symm_apply]