∀ {M : Type u_2} {N : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (x : Monoid.Coprod M N →* P),
  Monoid.Coprod.lift (x.comp Monoid.Coprod.inl, x.comp Monoid.Coprod.inr).1
      (x.comp Monoid.Coprod.inl, x.comp Monoid.Coprod.inr).2 =
    x