-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
mp :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair })) (β :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            ((binaryCoproductCocone X Y).ι.app { as := left : Discrete WalkingPair } ≫
              (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })) ∧
    Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair })) (β :=
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := right : Discrete WalkingPair }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              ((binaryCoproductCocone X Y).ι.app { as := right : Discrete WalkingPair } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })) ∧
      IsCompl (α :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := left : Discrete WalkingPair })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                ((binaryCoproductCocone X Y).ι.app { as := left : Discrete WalkingPair } ≫
                  (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                ((binaryCoproductCocone X Y).ι.app { as := right : Discrete WalkingPair } ≫
                  (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
⊢ Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair })) (β :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })) ∧
    Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair })) (β :=
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := right : Discrete WalkingPair }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })) ∧
      IsCompl (α :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := left : Discrete WalkingPair })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))

Tactic:
rw [← show _ = c.inl from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩,
        ← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.Types.binaryCoproductColimit