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✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
⊢ ↑(homTensorHomEquiv R M N P Q) x = ↑(homTensorHomMap R M N P Q) x
rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]