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.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:
exact (hl x).symm

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

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
l' : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).pt
h₁ : l' ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst
h : l' ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
h₂ :
  IsColimit (F := pair (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr)))
    (BinaryCofan.mk (P := Z) (↾fun (p : Types.PullbackObj f (↾Sum.inl)) ↦ (↑p : Z × PUnit.{u + 1}).1)
      (↾fun (p : Types.PullbackObj f (↾Sum.inr)) ↦ (↑p : Z × PUnit.{u + 1}).1))
⊢ IsColimit
    (BinaryCofan.mk
      (PullbackCone.fst
        (Types.pullbackLimitCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))).cone)
      (PullbackCone.fst
        (Types.pullbackLimitCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))).cone))

Tactic:
dsimp [Limits.Types.binaryCoproductCocone]

Premises used: CategoryTheory.Limits.Types.binaryCoproductCocone
-- 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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
x : Z
inl :
  Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) (Sum.inl PUnit.unit)
      (Sum.inl PUnit.unit) ∨
    Sum.inl PUnit.unit = Sum.inr PUnit.unit
inr :
  Sum.inr PUnit.unit = Sum.inl PUnit.unit ∨
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) (Sum.inr PUnit.unit)
      (Sum.inr PUnit.unit)
⊢ 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) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          x :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) ∨
    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) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          x :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})

Tactic:
rcases f x with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)

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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
x : Z
⊢ Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) (Sum.inl PUnit.unit)
      (Sum.inl PUnit.unit) ∨
    Sum.inl PUnit.unit = Sum.inr PUnit.unit

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- 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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
x : Z
⊢ Sum.inr PUnit.unit = Sum.inl PUnit.unit ∨
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) (Sum.inr PUnit.unit)
      (Sum.inr PUnit.unit)

Tactic:
Or.inr rfl

Premises used: Or.inr, rfl
-- 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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
x : Z
⊢ Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) (Sum.inl PUnit.unit)
      (Sum.inl PUnit.unit) ∨
    Sum.inl PUnit.unit = Sum.inr PUnit.unit

Tactic:
exacts [Or.inl rfl, Or.inr rfl]

Premises used: Or.inl, Or.inr, rfl
-- 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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
⊢ ∀ (x : (fun (X : Type u) ↦ X) Z),
    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) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) ∨
      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) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})

Tactic:
have : ∀ x, f x = Sum.inl PUnit.unit ∨ f x = Sum.inr PUnit.unit := by
      intro x
      rcases f x with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
      exacts [Or.inl rfl, Or.inr rfl]
-- 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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun (X : Type u) ↦ X) Z),
    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) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) ∨
      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) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})
p :
  { p : Z × PUnit.{u + 1} //
    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) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          p.1 :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }
⊢ 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) Z) →
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (↑p : Z × PUnit.{u + 1}).1 :
      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
    (Sum.inl (↑p : Z × PUnit.{u + 1}).2 : PUnit.{u + 1} ⊕ PUnit.{u + 1})

Tactic:
p.2

Premises used: Subtype.property
-- 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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun (X : Type u) ↦ X) Z),
    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) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) ∨
      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) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})
p :
  { p : Z × PUnit.{u + 1} //
    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) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          p.1 :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }
⊢ 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) Z) →
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (↑p : Z × PUnit.{u + 1}).1 :
      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
    (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})

Tactic:
convert! p.2

Premises used: Subtype.property
-- 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
rw :
  IsVanKampenColimit.{0, 0, u, u + 1} (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
    ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
⊢ FinitaryExtensive TopCat

Tactic:
rw [finitaryExtensive_iff_of_isTerminal TopCat.{u} _ TopCat.isTerminalPUnit _
      (TopCat.binaryCofanIsColimit _ _)]
-- 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
h₁ :
  ∀ {X' Y' : TopCat.{u}} (α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}))),
    αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) =
        (X'.binaryCofan Y').inl ≫ f →
      αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) =
          (X'.binaryCofan Y').inr ≫ f →
        IsPullback (X'.binaryCofan Y').inl αX f
            (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))) ∧
          IsPullback (X'.binaryCofan Y').inr αY f
            (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
h₂ :
  {Z : TopCat.{u}} →
    (f :
        Z ⟶
          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}))) →
      IsColimit (F :=
        pair
          (Cone.pt (F :=
            cospan (Y :=
              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                { as := WalkingPair.left : Discrete WalkingPair })
              f (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
            (TopCat.pullbackCone f (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))
          (Cone.pt (F :=
            cospan (Y :=
              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                { as := WalkingPair.right : Discrete WalkingPair })
              f (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
            (TopCat.pullbackCone f
              (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))))
        (BinaryCofan.mk
          (PullbackCone.fst
            (TopCat.pullbackCone f (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))
          (PullbackCone.fst
            (TopCat.pullbackCone f
              (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))))
⊢ IsVanKampenColimit.{0, 0, u, u + 1} (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
    ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))

Tactic:
apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => TopCat.binaryCofanIsColimit X Y) _
      fun f g => TopCat.pullbackConeIsLimit f g

Premises used: CategoryTheory.BinaryCofan.isVanKampen_mk, TopCat.pullbackConeIsLimit, TopCat.binaryCofanIsColimit
-- 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
h₁ :
  IsPullback (X'.binaryCofan Y').inl αX f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
h₂ :
  IsPullback (X'.binaryCofan Y').inr αY f
    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
⊢ IsPullback (X'.binaryCofan Y').inl αX f
      (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))) ∧
    IsPullback (X'.binaryCofan Y').inr αY f
      (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))

Tactic:
constructor