-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
this :
  ∀ (x : (fun (X : Type u) ↦ X) s.pt),
    ∃ (x_1 : X'),
      (fun (y : X') ↦
            Eq (α :=
              (fun (X : Type u) ↦ X)
                (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                    (a : (fun (X : Type u) ↦ X) s.pt) →
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                          { as := WalkingPair.left }))
                  x :
                (fun (X : Type u) ↦ X)
                  (Functor.obj
                    (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }))
              (Sum.inl y : X' ⊕ Y'))
          x_1 ∧
        ∀ (y : X'),
          (fun (y : X') ↦
                Eq (α :=
                  (fun (X : Type u) ↦ X)
                    (Functor.obj
                      (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                      { as := WalkingPair.left : Discrete WalkingPair }))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                        (a : (fun (X : Type u) ↦ X) s.pt) →
                          (fun (X : Type u) ↦ X)
                            (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                              { as := WalkingPair.left }))
                      x :
                    (fun (X : Type u) ↦ X)
                      (Functor.obj
                        (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                        { as := WalkingPair.left : Discrete WalkingPair }))
                  (Sum.inl y : X' ⊕ Y'))
              y →
            y = x_1
h₁ :
  (l : (x : s.pt) → X') →
    (hl :
        ∀ (x : s.pt),
          (fun (y : X') ↦
              Eq (α :=
                (fun (X : Type u) ↦ X)
                  (Functor.obj
                    (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                      (a : (fun (X : Type u) ↦ X) s.pt) →
                        (fun (X : Type u) ↦ X)
                          (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                            { as := WalkingPair.left }))
                    x :
                  (fun (X : Type u) ↦ X)
                    (Functor.obj
                      (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                      { as := WalkingPair.left : Discrete WalkingPair }))
                (Sum.inl y : X' ⊕ Y'))
            (l x)) →
      (hl' :
          ∀ (x : s.pt) (y : X'),
            (fun (y : X') ↦
                  Eq (α :=
                    (fun (X : Type u) ↦ X)
                      (Functor.obj
                        (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                        { as := WalkingPair.left : Discrete WalkingPair }))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                          (a : (fun (X : Type u) ↦ X) s.pt) →
                            (fun (X : Type u) ↦ X)
                              (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                                { as := WalkingPair.left }))
                        x :
                      (fun (X : Type u) ↦ X)
                        (Functor.obj
                          (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                          { as := WalkingPair.left : Discrete WalkingPair }))
                    (Sum.inl y : X' ⊕ Y'))
                y →
              y = l x) →
        { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt //
          l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst ∧
            l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd ∧
              ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt},
                m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst →
                  m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd → m = l }
⊢ { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt //
    l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd → m = l }

Tactic:
choose l hl hl' using this