no goals
A : Type ?u.66901
B : Type ?u.66904
G : Type ?u.66907
H : Type ?u.66910
M : Type u_3
N : Type u_1
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ ↑(comp (coprod f g) (inr M N)) x = ↑g x
simp [coprod_apply]