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
Z : TopCat
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}))))))

Tactic:
exact finitaryExtensiveTopCatAux Z f

Premises used: CategoryTheory.finitaryExtensiveTopCatAux
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
⊢ PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl

Tactic:
have : PreservesColimitsOfSize Gl := adj.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
van_kampen' : ∀ {X Y : D} (c : BinaryCofan.{v'', u''} X Y) (a : IsColimit c), IsVanKampenColimit c
⊢ FinitaryExtensive.{v'', u''} D

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
van_kampen' :
  IsVanKampenColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.precompose_isIso_iff
    (Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp

Premises used: CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, CategoryTheory.Adjunction.counit, CategoryTheory.Iso.trans, Iff.mp, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
h_obj :
  ∀ (X_1 : Discrete WalkingPair), (pair X Y ⋙ Gr).obj X_1 = Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) X_1
h_map :
  ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1),
    HEq ((pair X Y ⋙ Gr).map f) (β :=
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) X_1 ⟶
        Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) Y_1)
      (Functor.map (pair (Gr.obj X) (Gr.obj Y)) f)
⊢ pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)

Tactic:
apply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ (pair X Y ⋙ Gr).obj { as := WalkingPair.left : Discrete WalkingPair } =
    Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ (pair X Y ⋙ Gr).obj { as := WalkingPair.right : Discrete WalkingPair } =
    Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ HEq
    ((pair X Y ⋙ Gr).map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := WalkingPair.left : Discrete WalkingPair }.as =
                { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair }.as) } :
        ULift.{0, 0}
          (PLift
            ({ as := WalkingPair.left : Discrete WalkingPair }.as =
              { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair }.as)) })
    (β :=
    Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y))
        { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair })
    (Functor.map (pair (Gr.obj X) (Gr.obj Y)) { down := { down := ⋯ } })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ HEq
    ((pair X Y ⋙ Gr).map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := WalkingPair.right : Discrete WalkingPair }.as =
                { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair }.as) } :
        ULift.{0, 0}
          (PLift
            ({ as := WalkingPair.right : Discrete WalkingPair }.as =
              { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair }.as)) })
    (β :=
    Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y))
        { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair })
    (Functor.map (pair (Gr.obj X) (Gr.obj Y)) { down := { down := ⋯ } })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)

Tactic:
have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
rw :
  ∀ (Z : C) (i : Discrete WalkingPair)
    (f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))),
    PreservesLimit (cospan f (NatTrans.app (Cocone.ι (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))) i)) Gl
⊢ ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))
left :
  PreservesLimit
    (cospan (Y := Gr.obj X) f
      (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } :
        Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
          colimit.{0, 0, v, u} (pair (Gr.obj X) (Gr.obj Y))))
    Gl
⊢ PreservesLimit
    (cospan (Y :=
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))))
        { as := WalkingPair.left : Discrete WalkingPair }))
    Gl

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))
right :
  PreservesLimit
    (cospan (Y := Gr.obj Y) f
      (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } :
        Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
          colimit.{0, 0, v, u} (pair (Gr.obj X) (Gr.obj Y))))
    Gl
⊢ PreservesLimit
    (cospan (Y :=
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))))
        { as := WalkingPair.right : Discrete WalkingPair }))
    Gl

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))
⊢ PreservesLimit
    (cospan (Y := Gr.obj X) f
      (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } :
        Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
          colimit.{0, 0, v, u} (pair (Gr.obj X) (Gr.obj Y))))
    Gl

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))
⊢ PreservesLimit
    (cospan (Y := Gr.obj Y) f
      (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } :
        Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
          colimit.{0, 0, v, u} (pair (Gr.obj X) (Gr.obj Y))))
    Gl

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl

Tactic:
have : ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
        PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl := by
    have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
    rw [this]
    rintro Z ⟨_ | _⟩ f <;> dsimp <;> infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this :
  ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
⊢ IsVanKampenColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)

Tactic:
((FinitaryExtensive.vanKampen _ (colimit.isColimit <| pair X Y ⋙ _)).map_reflective
    adj).of_iso (IsColimit.uniqueUpToIso ?_ ?_)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.IsVanKampenColimit.map_reflective, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this :
  ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
van_kampen' : IsColimit (Gl.mapCocone (colimit.cocone (pair X Y ⋙ Gr)))
van_kampen'₁ :
  IsColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)
⊢ IsVanKampenColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)

Tactic:
refine ((FinitaryExtensive.vanKampen _ (colimit.isColimit <| pair X Y ⋙ _)).map_reflective
    adj).of_iso (IsColimit.uniqueUpToIso ?_ ?_)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.IsVanKampenColimit.map_reflective, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this :
  ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
⊢ IsColimit (Gl.mapCocone (colimit.cocone (pair X Y ⋙ Gr)))

Tactic:
exact isColimitOfPreserves Gl (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isColimitOfPreserves