no goals
A : Type ?u.73446
B : Type ?u.73449
G : Type ?u.73452
H : Type ?u.73455
M : Type u_3
N : Type u_4
P : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
f✝ : M →* P
g✝ : N →* P
Q : Type u_1
inst✝ : CommMonoid 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