-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst : Mono f
⊢ Nonempty.{u + 2}
    (IsColimit (F :=
      pair X
        { x : (fun (X : Type u) ↦ X) Y //
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) X)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
            x })
      (BinaryCofan.mk f
        (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
            Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
              (Set.range (ι := (fun (X : Type u) ↦ X) X)
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
              x))))
have h : Injective (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (pair X
          { x : (fun (X : Type u) ↦ X) Y //
            Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
              (Set.range (ι := (fun (X : Type u) ↦ X) X)
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
              x })
        { as := left : Discrete WalkingPair }))
    (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F :=
            pair X
              { x : (fun (X : Type u) ↦ X) Y //
                Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                  (Set.range (ι := (fun (X : Type u) ↦ X) X)
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                  x })
            (BinaryCofan.mk f
              (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                    (Set.range (ι := (fun (X : Type u) ↦ X) X)
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                    x)))))
        { as := left : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (BinaryCofan.inl
            (BinaryCofan.mk f
              (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                    (Set.range (ι := (fun (X : Type u) ↦ X) X)
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                    x))))) :
      (a :
          (fun (X : Type u) ↦ X)
            ((pair X
                  { x : (fun (X : Type u) ↦ X) Y //
                    x ∈
                      (Set.range
                          (⇑(ConcreteCategory.hom f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
              { as := left })) →
        (fun (X : Type u) ↦ X)
          (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := left })) ∧
  Injective (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (pair X
            { x : (fun (X : Type u) ↦ X) Y //
              Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                (Set.range (ι := (fun (X : Type u) ↦ X) X)
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                x })
          { as := right : Discrete WalkingPair }))
      (β :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair X
                { x : (fun (X : Type u) ↦ X) Y //
                  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                    (Set.range (ι := (fun (X : Type u) ↦ X) X)
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                    x })
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x)))))
          { as := right : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (BinaryCofan.inr
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x))))) :
        (a :
            (fun (X : Type u) ↦ X)
              ((pair X
                    { x : (fun (X : Type u) ↦ X) Y //
                      x ∈
                        (Set.range
                            (⇑(ConcreteCategory.hom f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                { as := right })) →
          (fun (X : Type u) ↦ X)
            (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := right })) ∧
    IsCompl (α :=
      Set
        ((fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F :=
                pair X
                  { x : (fun (X : Type u) ↦ X) Y //
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x })
                (BinaryCofan.mk f
                  (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                        (Set.range (ι := (fun (X : Type u) ↦ X) X)
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                        x)))))
            { as := left : Discrete WalkingPair })))
      (Set.range (ι :=
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (pair X
              { x : (fun (X : Type u) ↦ X) Y //
                Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                  (Set.range (ι := (fun (X : Type u) ↦ X) X)
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                  x })
            { as := left : Discrete WalkingPair }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (BinaryCofan.inl
                (BinaryCofan.mk f
                  (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                        (Set.range (ι := (fun (X : Type u) ↦ X) X)
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                        x))))) :
          (a :
              (fun (X : Type u) ↦ X)
                ((pair X
                      { x : (fun (X : Type u) ↦ X) Y //
                        x ∈
                          (Set.range
                              (⇑(ConcreteCategory.hom f) :
                                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                  { as := left })) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := left })))
      (Set.range (ι :=
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (pair X
              { x : (fun (X : Type u) ↦ X) Y //
                Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                  (Set.range (ι := (fun (X : Type u) ↦ X) X)
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                  x })
            { as := right : Discrete WalkingPair }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (BinaryCofan.inr
                (BinaryCofan.mk f
                  (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                        (Set.range (ι := (fun (X : Type u) ↦ X) X)
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                        x))))) :
          (a :
              (fun (X : Type u) ↦ X)
                ((pair X
                      { x : (fun (X : Type u) ↦ X) Y //
                        x ∈
                          (Set.range
                              (⇑(ConcreteCategory.hom f) :
                                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                  { as := right })) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := right })))
Tactic: rw [binaryCofan_isColimit_iff]