case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (fst R B C) (prod f g) = f
ext
no goals
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑(comp (fst R B C) (prod f g)) x✝ = ↑f x✝
rfl