no goals
A : Type ?u.68969
B : Type ?u.68972
G : Type ?u.68975
H : Type ?u.68978
M : Type u_2
N : Type u_1
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f✝ : M →* P
g : N →* P
f : M × N →* P
x : M × N
⊢ ↑(coprod (comp f (inl M N)) (comp f (inr M N))) x = ↑f x
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]