no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1289962
inst✝¹³ : Monoid R'
R'' : Type ?u.1289968
inst✝¹² : Semiring R''
M : Type u_4
N : Type u_5
P : Type u_2
Q : Type u_6
S : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g✝ : P →ₗ[R] Q
f✝ : N →ₗ[R] P
f' : P →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ comp (rTensor Q f') (map f g) = map (comp f' f) g
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]