-- 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.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : (x : s.pt) → Y'
hl :
  ∀ (x : s.pt),
    (fun (y : Y') ↦
        Eq (α :=
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
              { as := WalkingPair.right : 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.right }))
              x :
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.right : Discrete WalkingPair }))
          (Sum.inr y : X' ⊕ Y'))
      (l x)
hl' :
  ∀ (x : s.pt) (y : Y'),
    (fun (y : Y') ↦
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.right : 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.right }))
                x :
              (fun (X : Type u) ↦ X)
                (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }))
            (Sum.inr y : X' ⊕ Y'))
        y →
      y = l x
h₁ : ↾l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst
⊢ { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).pt //
    l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).snd = s.snd → m = l }
have h₂ : ∀ {l' : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).pt}
  (h₁ : l' ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).fst = s.fst),
  l' ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).snd = s.snd → l' = ↾l
Tactic: refine ⟨↾l, ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩