awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : 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}))
l : (x : s.pt) → X'
hl :
  ∀ (x : s.pt),
    (fun (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'))
      (l x)
hl' :
  ∀ (x : s.pt) (y : X'),
    (fun (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'))
        y →
      y = l x
l' : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt
h₁ : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst
h : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd
x : s.pt
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) l').toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) (↾l)).toFun x

Tactic:
hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- 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' : 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}))
l : (x : s.pt) → X'
hl :
  ∀ (x : s.pt),
    (fun (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'))
      (l x)
hl' :
  ∀ (x : s.pt) (y : X'),
    (fun (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'))
        y →
      y = l x
l' : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt
h₁ : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst
h : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd
x : s.pt
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) l').toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) (↾l)).toFun x

Tactic:
exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- 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' : 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
⊢ IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux', CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, Eq.symm
-- 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' : 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
h₁ :
  (s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))) →
    { 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 }
⊢ IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
-- 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' : 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}))
x : s.pt
val : X'
h :
  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.inl val : X' ⊕ Y')
⊢ Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
          (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        ((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 })) :
      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
          (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl val) :
      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)

Tactic:
apply_fun f at h
-- 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' : 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}))
x : s.pt
val : X'
h :
  Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
          (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        ((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 })) :
      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
          (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl val) :
      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
⊢ ∃! y : Y', Sum.inl val = Sum.inr y

Tactic:
cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Eq.trans
-- 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' : 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}))
x : s.pt
val : Y'
h :
  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 val : X' ⊕ Y')
⊢ ∃! 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 }))
      (Sum.inr val) (Sum.inr y)

Tactic:
simp
-- 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' : 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}))
⊢ ∀ (x : (fun (X : Type u) ↦ X) s.pt),
    ∃! 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')

Tactic:
have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · simp
-- 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' : 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₁ :
  ∀ (x : s.pt),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst)).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) s.fst).toFun x
⊢ ↾l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst

Tactic:
ext x
-- 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' : 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
x : s.pt
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) s.fst).toFun x

Tactic:
(hl x).symm

Premises used: Eq.symm