-- 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.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑Y' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑Y' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.right : 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.right }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }) :
              Type u))
          (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑Y' : Type u)),
    (fun (y : (↑Y' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.right : 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.right }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.right : Discrete WalkingPair }) :
                Type u))
            (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
h :
  ((↑X' : Type u) ⊕ (↑Y' : Type u)) =
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }) :
        Type u) →
    Sum.inr ∘ l = (TopCat.Hom.hom s.fst).toFun
⊢ Continuous (Y := (↑X' : Type u) ⊕ (↑Y' : Type u)) (Sum.inr ∘ l)

Tactic:
convert! s.fst.hom.2 using 1

Premises used: CategoryTheory.Limits.PullbackCone.fst, ContinuousMap.continuous_toFun, TopCat.Hom.hom