awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : FinitaryExtensive.{v, u} C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ Mono c.inl

Tactic:
FinitaryExtensive.mono_inr_of_isColimit (BinaryCofan.isColimitFlip hc)

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit, CategoryTheory.Limits.BinaryCofan.isColimitFlip, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : FinitaryExtensive.{v, u} C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ IsPullback (P := initial.{v, u} C)
    (initial.to (Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (initial.to (Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })) c.inl c.inr

Tactic:
BinaryCofan.isPullback_initial_to_of_isVanKampen (FinitaryExtensive.vanKampen c hc)

Premises used: CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen
-- 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
inst_3 : FinitaryPreExtensive.{v, u} C
dsimp : IsIso.{v, u} (𝟙 (initial.{v, u} C))
⊢ IsIso.{v, u} (Y :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))

Tactic:
dsimp
-- 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
inst_3 : FinitaryPreExtensive.{v, u} C
⊢ IsIso.{v, u} (𝟙 (initial.{v, u} C))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
⊢ FinitaryExtensive.{v, u} C ↔ IsVanKampenColimit c₀

Tactic:
⟨fun H => H.van_kampen' c₀ hc₀, fun H => ?_⟩

Premises used: CategoryTheory.FinitaryExtensive.van_kampen', Iff.intro
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
refine : ∀ (H : IsVanKampenColimit c₀), FinitaryExtensive.{v, u} C
⊢ FinitaryExtensive.{v, u} C ↔ IsVanKampenColimit c₀

Tactic:
refine ⟨fun H => H.van_kampen' c₀ hc₀, fun H => ?_⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H : IsVanKampenColimit c₀
van_kampen' : ∀ {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c), IsVanKampenColimit c
⊢ FinitaryExtensive.{v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H : IsVanKampenColimit c₀
van_kampen' :
  ∀
    (H :
      ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
        αX ≫ c₀.inl = c'.inl ≫ f →
          αY ≫ c₀.inr = c'.inr ≫ f →
            (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr))
    {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c) {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X)
    (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
⊢ ∀ {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c), IsVanKampenColimit c

Tactic:
simp_rw [BinaryCofan.isVanKampen_iff] at H ⊢

Premises used: CategoryTheory.BinaryCofan.isVanKampen_iff
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
van_kampen' :
  ∀
    (d :
      c.pt ⟶
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
          { as := WalkingPair.left : Discrete WalkingPair })
    (hd : c.inl ≫ d = HT.from X ≫ c₀.inl) (hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr),
    Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
obtain ⟨d, hd, hd'⟩ :=
    Limits.BinaryCofan.IsColimit.desc' hc (HT.from _ ≫ c₀.inl) (HT.from _ ≫ c₀.inr)

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.Limits.BinaryCofan.inl, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.BinaryCofan.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
rw : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ c.inl ≫ d
rw₁ : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ HT.from X ≫ c₀.inl
rw₂ rw₃ : αX ≫ HT.from X ≫ c₀.inl = αX ≫ HT.from X ≫ c₀.inl
⊢ (αX ≫ HT.from X) ≫ c₀.inl = c'.inl ≫ f ≫ d

Tactic:
rw [← reassoc_of% hX, hd, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
rw : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ c.inr ≫ d
rw₁ : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ HT.from Y ≫ c₀.inr
rw₂ rw₃ : αY ≫ HT.from Y ≫ c₀.inr = αY ≫ HT.from Y ≫ c₀.inr
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = c'.inr ≫ f ≫ d

Tactic:
rw [← reassoc_of% hY, hd', Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
van_kampen' :
  IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
rw [H c' (αX ≫ HT.from _) (αY ≫ HT.from _) (f ≫ d) (by rw [← reassoc_of% hX, hd, Category.assoc])
      (by rw [← reassoc_of% hY, hd', Category.assoc])]

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ IsPullback c.inl (HT.from X) d c₀.inl

Tactic:
obtain ⟨hl, hr⟩ := (H c (HT.from _) (HT.from _) d hd.symm hd'.symm).mp ⟨hc⟩

Premises used: CategoryTheory.Limits.IsTerminal.from, Nonempty.intro, Iff.mp, Eq.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
⊢ IsPullback c.inr (HT.from Y) d c₀.inr

Tactic:
obtain ⟨hl, hr⟩ := (H c (HT.from _) (HT.from _) d hd.symm hd'.symm).mp ⟨hc⟩

Premises used: CategoryTheory.Limits.IsTerminal.from, Nonempty.intro, Iff.mp, Eq.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
hr : IsPullback c.inr (HT.from Y) d c₀.inr
van_kampen' :
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
van_kampen'₁ van_kampen'₂ :
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
rw [hl.paste_vert_iff hX.symm, hr.paste_vert_iff hY.symm]

Premises used: CategoryTheory.IsPullback.paste_vert_iff, 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
rw : IsVanKampenColimit (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})
⊢ FinitaryExtensive (Type u)

Tactic:
rw [finitaryExtensive_iff_of_isTerminal (Type u) PUnit Types.isTerminalPUnit _
      (Types.binaryCoproductColimit _ _)]
-- 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' : 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),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
h₂ :
  {Z : Type u} →
    (f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) →
      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))
⊢ IsVanKampenColimit (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})

Tactic:
apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => Types.binaryCoproductColimit X Y) _
      fun f g => (Limits.Types.pullbackLimitCone f g).2

Premises used: CategoryTheory.Limits.Types.pullbackLimitCone, CategoryTheory.BinaryCofan.isVanKampen_mk, CategoryTheory.Limits.LimitCone.isLimit, CategoryTheory.Limits.Types.binaryCoproductColimit
-- 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' : Type u
h₁ :
  ∀ {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),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ ∀ {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),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
_
-- 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
h₁ :
  ∀ (α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),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ ∀ (α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),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
_
-- 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}
h₁ :
  ∀ (αY : Y' ⟶ PUnit.{u + 1})
    (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ ∀ (αY : Y' ⟶ PUnit.{u + 1})
    (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
_
-- 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₁ :
  IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
h₂ :
  IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
      (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
    IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
      (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
constructor
-- 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.inl (Types.binaryCoproductCocone X' Y')) αX f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

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

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux', CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, Eq.symm