-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
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 })))
⊢ 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 })))
have 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)
Tactic: constructor