-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X Y : Type u
c : BinaryCofan X Y
h₁ :
  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 }))
h₂ :
  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 }))
h₃ :
  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 })))
this :
  ∀
    (x :
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })),
    Membership.mem (γ :=
        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 })))
        x ∨
      Membership.mem (γ :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := right : Discrete WalkingPair })))
        (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 })))
        x
mpr : {T : Type u} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)
mpr₁ :
  ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inl ≫
        ↾fun (x : c.pt) ↦
          if h :
              Membership.mem (γ :=
                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 })))
                x then
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) T)
              (((Equiv.ofInjective
                        (⇑(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 }))
                        h₁).symm :
                    (a :
                        (↑(Set.range
                              (⇑(ConcreteCategory.hom 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 }))) :
                          Type u)) →
                      (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                  (Subtype.mk (p :=
                    fun
                      (x :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := left : Discrete WalkingPair })) ↦
                    Membership.mem (γ :=
                      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 })))
                      x)
                    x h) :
                (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          else
            (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) T)
              (((Equiv.ofInjective
                        (⇑(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 }))
                        h₂).symm :
                    (a :
                        (↑(Set.range
                              (⇑(ConcreteCategory.hom 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 }))) :
                          Type u)) →
                      (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                  (Subtype.mk (p :=
                    fun
                      (x :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := right : Discrete WalkingPair })) ↦
                    Membership.mem (γ :=
                      Set
                        ((fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := right : Discrete WalkingPair })))
                      (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 })))
                      x)
                    x ⋯) :
                (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))) =
      f
mpr₂ :
  ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inr ≫
        ↾fun (x : c.pt) ↦
          if h :
              Membership.mem (γ :=
                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 })))
                x then
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) T)
              (((Equiv.ofInjective
                        (⇑(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 }))
                        h₁).symm :
                    (a :
                        (↑(Set.range
                              (⇑(ConcreteCategory.hom 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 }))) :
                          Type u)) →
                      (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                  (Subtype.mk (p :=
                    fun
                      (x :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := left : Discrete WalkingPair })) ↦
                    Membership.mem (γ :=
                      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 })))
                      x)
                    x h) :
                (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          else
            (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) T)
              (((Equiv.ofInjective
                        (⇑(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 }))
                        h₂).symm :
                    (a :
                        (↑(Set.range
                              (⇑(ConcreteCategory.hom 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 }))) :
                          Type u)) →
                      (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                  (Subtype.mk (p :=
                    fun
                      (x :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := right : Discrete WalkingPair })) ↦
                    Membership.mem (γ :=
                      Set
                        ((fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := right : Discrete WalkingPair })))
                      (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 })))
                      x)
                    x ⋯) :
                (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))) =
      g
⊢ Nonempty (IsColimit c)
have mpr₃ : ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T),
  c.inl ≫ m = f →
    c.inr ≫ m = g →
      m =
        ↾fun (x : c.pt) ↦
          if h :
              Membership.mem (γ :=
                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 })))
                x then
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) T)
              (((Equiv.ofInjective
                        (⇑(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 }))
                        h₁).symm :
                    (a :
                        (↑(Set.range
                              (⇑(ConcreteCategory.hom 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 }))) :
                          Type u)) →
                      (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                  (Subtype.mk (p :=
                    fun
                      (x :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := left : Discrete WalkingPair })) ↦
                    Membership.mem (γ :=
                      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 })))
                      x)
                    x h) :
                (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          else
            (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) T)
              (((Equiv.ofInjective
                        (⇑(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 }))
                        h₂).symm :
                    (a :
                        (↑(Set.range
                              (⇑(ConcreteCategory.hom 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 }))) :
                          Type u)) →
                      (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                  (Subtype.mk (p :=
                    fun
                      (x :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := right : Discrete WalkingPair })) ↦
                    Membership.mem (γ :=
                      Set
                        ((fun (X : Type u) ↦ X)
                          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                            { as := right : Discrete WalkingPair })))
                      (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 })))
                      x)
                    x sorry) :
                (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
Tactic: refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩