-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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})))
x : (↑s.pt : Type u)
inl :
  ∀ (val : (↑X' : Type u))
    (h :
      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.inl val : (↑X' : Type u) ⊕ (↑Y' : Type u))),
    ∃! y : (↑Y' : Type u), Sum.inl val = Sum.inr y
⊢ ∃! 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))
have inr : ∀ (val : (↑Y' : Type u))
  (h :
    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 val : (↑X' : Type u) ⊕ (↑Y' : Type u))),
  ∃! y : (↑Y' : Type u),
    Eq (α :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }) :
        Type u))
      (Sum.inr val) (Sum.inr y)
Tactic: rcases h : s.fst x with val | val