-- 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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
this :
  ∀ (x : (↑s.pt : Type u)),
    ∃ (x_1 : (↑X' : Type u)),
      (fun (y : (↑X' : Type u)) ↦
            Eq (α :=
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) s.fst :
                    (a : (↑s.pt : Type u)) →
                      (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                            { as := WalkingPair.left }) :
                        Type u))
                  x :
                (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                      { as := WalkingPair.left : Discrete WalkingPair }) :
                  Type u))
              (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
          x_1 ∧
        ∀ (y : (↑X' : Type u)),
          (fun (y : (↑X' : Type u)) ↦
                Eq (α :=
                  (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                        { as := WalkingPair.left : Discrete WalkingPair }) :
                    Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) s.fst :
                        (a : (↑s.pt : Type u)) →
                          (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                                { as := WalkingPair.left }) :
                            Type u))
                      x :
                    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                          { as := WalkingPair.left : Discrete WalkingPair }) :
                      Type u))
                  (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
              y →
            y = x_1
h₁ :
  (l : (x : (↑s.pt : Type u)) → (↑X' : Type u)) →
    (hl :
        ∀ (x : (↑s.pt : Type u)),
          (fun (y : (↑X' : Type u)) ↦
              Eq (α :=
                (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                      { as := WalkingPair.left : Discrete WalkingPair }) :
                  Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) s.fst :
                      (a : (↑s.pt : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                              { as := WalkingPair.left }) :
                          Type u))
                    x :
                  (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                        { as := WalkingPair.left : Discrete WalkingPair }) :
                    Type u))
                (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
            (l x)) →
      (hl' :
          ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
            (fun (y : (↑X' : Type u)) ↦
                  Eq (α :=
                    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                          { as := WalkingPair.left : Discrete WalkingPair }) :
                      Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) s.fst :
                          (a : (↑s.pt : Type u)) →
                            (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                                  { as := WalkingPair.left }) :
                              Type u))
                        x :
                      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u))
                    (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
                y →
              y = l x) →
        { l : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).pt //
          l ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).fst = s.fst ∧
            l ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).snd = s.snd ∧
              ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).pt},
                m ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).fst = s.fst →
                  m ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).snd = s.snd → m = l }
⊢ { l : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).pt //
    l ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).pt},
          m ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).snd = s.snd → m = l }

Tactic:
choose l hl hl' using this