-- 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' : 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}))
x : s.pt
inl :
  ∀ (val : X')
    (h :
      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 val : X' ⊕ Y')),
    ∃! 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 }))
        (Sum.inl val) (Sum.inl y)
⊢ ∃! 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')
have inr : ∀ (val : Y')
  (h :
    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.inr val : X' ⊕ Y')),
  ∃! y : X', Sum.inr val = Sum.inl y
Tactic: rcases h : s.fst x with val | val