no goals
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : End R M
g : End R N
⊢ ↑endTensorEndAlgHom (f ⊗ₜ[R] g) = map f g
simp only [endTensorEndAlgHom, Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply,
  homTensorHomMap_apply]