no goals
A : Type ?u.44652
B : Type ?u.44655
G : Type ?u.44658
H : Type ?u.44661
M : Type u_3
N : Type u_4
P : Type u_2
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : CommSemigroup P
f✝ : M →ₙ* P
g✝ : N →ₙ* P
Q : Type u_1
inst✝ : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ ↑(comp h (coprod f g)) x = ↑(coprod (comp h f) (comp h g)) x
simp