∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (X : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] {X_1 Y : CategoryTheory.Under X} (g : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.coprodMonad X).map g.right)
      { A := Y.right, a := CategoryTheory.Limits.coprod.desc Y.hom (CategoryTheory.CategoryStruct.id Y.right),
          unit := ⋯, assoc := ⋯ }.a =
    CategoryTheory.CategoryStruct.comp
      { A := X_1.right, a := CategoryTheory.Limits.coprod.desc X_1.hom (CategoryTheory.CategoryStruct.id X_1.right),
          unit := ⋯, assoc := ⋯ }.a
      g.right