-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
mp :
  Nonempty (IsColimit c) →
    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 })))
mpr mpr₁ :
  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 }))) →
    Nonempty (IsColimit c)
⊢ Nonempty (IsColimit c) ↔
    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:
classical
    constructor
    · rintro ⟨h⟩
      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⟩]
      dsimp [binaryCoproductCocone]
      refine
        ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inl_injective,
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inr_injective, ?_⟩
      rw [types_comp, Set.range_comp, ← eq_compl_iff_isCompl, types_comp]
      dsimp
      rw [Set.range_comp _ Sum.inr, ← dsimp% [Iso.toEquiv] Set.image_compl_eq
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
      simp
    · rintro ⟨h₁, h₂, h₃⟩
      have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr := by
        rw [eq_compl_iff_isCompl.mpr h₃.symm]
        exact fun _ => or_not
      refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩
      · intro T f g
        refine ↾fun x => ?_
        exact
          if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
          else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)
      · intro T f g
        ext x
        simp
      · intro T f g
        ext x
        dsimp
        simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff,
          forall_exists_index]
        intro y e
        have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
        rw [disjoint_iff.mp h₃.1] at this
        exact this.elim
      · rintro T _ _ m rfl rfl
        ext x
        simp only [TypeCat.Fun.toFun_apply, Functor.const_obj_obj, pair_obj_left, Set.mem_range,
          comp_apply, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
        split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

Premises used: Set.range_comp, Set.mem_range, CategoryTheory.Iso.toEquiv, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pair_obj_right, TypeCat.Fun.coe_mk, forall_exists_index, CategoryTheory.types_comp, dite_eq_right_iff, TypeCat.Fun.toFun_apply, Equiv.ofInjective_symm_apply, eq_compl_iff_isCompl, Subtype.mk, congr_arg, CategoryTheory.comp_apply, Sum.inr, CategoryTheory.Limits.Types.binaryCoproductCocone, CategoryTheory.Limits.BinaryCofan.inl, CategoryTheory.Limits.pair_obj_left, Set.range, CategoryTheory.Functor.const_obj_obj, Eq.symm, CategoryTheory.ConcreteCategory.hom_ofHom, DFunLike.coe, Equiv.apply_ofInjective_symm, rfl