no goals
N : Type u_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.405020
M₆ : Type ?u.405023
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ LinearMap.comp (LinearMap.snd R N M) ↑(prodComm R M N) = LinearMap.fst R M N
ext <;> simp