no goals
A : Type ?u.64869
B : Type ?u.64872
G : Type ?u.64875
H : Type ?u.64878
M : Type u_1
N : Type u_3
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ ↑(comp (coprod f g) (inl M N)) x = ↑f x
simp [coprod_apply]