no goals
R : Type u
A : Type v
B : Type w
C : Type w₁
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : DistribMulAction R B
inst✝¹ : NonUnitalNonAssocSemiring C
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ comp (snd R B C) (prod f g) = g
rfl