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_1 Y : C
inst_3 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_4 : Finite ι
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
i j : ι
e : i ≠ j
s : PullbackCone (c.inj i) (c.inj j)
hs : IsLimit s
⊢ Nonempty (IsInitial.{v, u} s.pt)

Tactic:
exact ⟨initialIsInitial.ofIso ((FinitaryExtensive.isPullback_initial_to hc ⟨i⟩ ⟨j⟩
      (by simpa)).isoIsPullback _ _ (IsPullback.of_isLimit hs))⟩
-- 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_1 Y_1 : C
inst_3 : FinitaryPreExtensive.{v, u} C
X Z : C
α : Type u_1
f : X ⟶ Z
Y : (a : α) → C
i : (a : α) → Y a ⟶ Z
inst_4 : Finite α
hi : IsIso (X := sigmaObj.{u_1, v, u} Y) (Sigma.desc i)
a : α
hc : IsColimit (Cofan.mk Z i)
⊢ HasPullback f (i a)

Tactic:
apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i)

Premises used: CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct
-- 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_1 Y_1 : C
inst_3 : FinitaryPreExtensive.{v, u} C
X Z : C
α : Type u_1
f : X ⟶ Z
Y : (a : α) → C
i : (a : α) → Y a ⟶ Z
inst_4 : Finite α
hi : IsIso (X := sigmaObj.{u_1, v, u} Y) (Sigma.desc i)
a : α
⊢ IsColimit (Cofan.mk Z i)

Tactic:
exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) (i := hi)

Premises used: CategoryTheory.Limits.IsColimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
apply : Nonempty (IsColimit c)
⊢ IsIso.{v, u} (C := C) (X := sigmaObj.{0, v, u} fun (x : α) ↦ pullback f (π x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst f (π x))

Tactic:
apply c.nonempty_isColimit_iff_isIso_sigmaDesc.mp

Premises used: Iff.mp, CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
⊢ IsUniversalColimit (Cofan.mk X π)

Tactic:
have hau : IsUniversalColimit (Cofan.mk X π) := FinitaryPreExtensive.isUniversal_finiteCoproducts
    ((Cofan.nonempty_isColimit_iff_isIso_sigmaDesc _).mpr hπ).some
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ 𝟙 Y ≫ f = f ≫ 𝟙 (Cofan.mk X π).pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ ∀ (i : α), (Cofan.mk X π).inj i ≫ 𝟙 (Cofan.mk X π).pt = π i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ ∀ (i : α),
    c.inj i ≫ Iso.hom (Iso.refl c.pt) ≫ (PullbackCone.mk (𝟙 Y) f ⋯).fst = PullbackCone.fst (limit.cone (cospan f (π i)))

Tactic:
simp [c]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ ∀ (i : α),
    c.inj i ≫ Iso.hom (Iso.refl c.pt) ≫ (PullbackCone.mk (𝟙 Y) f ⋯).snd =
      PullbackCone.snd (limit.cone (cospan f (π i))) ≫ (Cofan.mk X π).inj i

Tactic:
simp [pullback.condition, c]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
refine : (i : α) → IsLimit (limit.cone (cospan f (π i)))
⊢ Nonempty (IsColimit c)

Tactic:
refine hau.nonempty_isColimit_of_pullbackCone_left _ (𝟙 _) _ _ (fun i ↦ ?_)
    (PullbackCone.mk (𝟙 _) f (by simp)) (IsPullback.id_horiz f).isLimit _ (Iso.refl _)
    (by simp) (by simp [c]) (by simp [pullback.condition, c])

Premises used: CategoryTheory.IsPullback.id_horiz, CategoryTheory.CategoryStruct.id, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
α : Type
inst_2 : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (X := sigmaObj.{0, v, u} Z) (Sigma.desc π)
c : Cofan.{0, v, u} (C := C) fun (x : α) ↦ pullback f (π x) := Cofan.mk Y fun (x : α) ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
i : α
⊢ IsLimit (limit.cone (cospan f (π i)))

Tactic:
exact pullback.isLimit _ _

Premises used: CategoryTheory.Limits.pullback.isLimit
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
p : ι × ι'
⊢ Eq (α := X p.1 ⟶ S) (f p.1 ≫ 𝟙 S) (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} X) (Sigma.ι X p.1) (Sigma.desc f))

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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
p : ι × ι'
⊢ Eq (α := Y p.2 ⟶ S) (g p.2 ≫ 𝟙 S) (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} Y) (Sigma.ι Y p.2) (Sigma.desc g))

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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
apply : Nonempty (IsColimit c)
⊢ IsIso.{v, u} (C := C) (X := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (Y :=
    pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    (Sigma.desc fun (p : ι × ι') ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯)

Tactic:
apply c.nonempty_isColimit_iff_isIso_sigmaDesc.mp

Premises used: Iff.mp, CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ Nonempty (IsColimit c)

Tactic:
IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, CategoryTheory.Limits.limit, CategoryTheory.Limits.Sigma.desc, CategoryTheory.Limits.pullback.cone
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
refine_1 :
  IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
refine_2 :
  IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
    (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)
refine_3 :
  IsLimit (F :=
    cospan (X :=
      Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
        (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i))
      (Y :=
      Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
        (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i))
      (Sigma.desc f) (Sigma.desc g))
    (pullback.cone (Sigma.desc f) (Sigma.desc g))
⊢ Nonempty (IsColimit c)

Tactic:
refine IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
      (a := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i)
      ?_ ?_ f g (Sigma.desc f) (Sigma.desc g) (fun i j ↦ (pullback.cone (f i) (g j)))
      (fun i j ↦ pullback.isLimit (f i) (g j)) (pullback.cone _ _) ?_ (Iso.refl _)

Premises used: CategoryTheory.Limits.pullback.isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, CategoryTheory.Limits.Sigma.desc, CategoryTheory.Limits.pullback.cone
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)

Tactic:
FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)

Tactic:
exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
    (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)

Tactic:
FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
    (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)

Tactic:
exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- 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_1 Y_1 : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_5 : Finite ι
inst_6 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan (C := C) fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2) :=
  Cofan.mk (pullback (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y) (Sigma.desc f) (Sigma.desc g))
    fun (p : ι × ι') ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsLimit (F :=
    cospan (X :=
      Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ X i)
        (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i))
      (Y :=
      Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor fun (i : ι') ↦ Y i)
        (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i))
      (Sigma.desc f) (Sigma.desc g))
    (pullback.cone (Sigma.desc f) (Sigma.desc g))

Tactic:
exact pullback.isLimit (Sigma.desc f) (Sigma.desc g)

Premises used: CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsPullback (P :=
    Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
    (X :=
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor X)
      (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i))
    (Y :=
    Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor Y)
      (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i))
    (Cofan.IsColimit.desc (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      fun (p : ι × ι') ↦
      pullback.fst (f p.1) (g p.2) ≫ Cofan.inj (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i) p.1)
    (Cofan.IsColimit.desc (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      fun (p : ι × ι') ↦
      pullback.snd (f p.1) (g p.2) ≫ Cofan.inj (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i) p.2)
    (Sigma.desc f) (Sigma.desc g)

Tactic:
IsUniversalColimit.isPullback_prod_of_isColimit (d :=
      Cofan.mk _ (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (hd :=
      coproductIsCoproduct (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (a :=
      Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) ?_ ?_ f g
      (Sigma.desc f) (Sigma.desc g) (fun i j ↦ IsPullback.of_hasPullback (f i) (g j))

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Limits.coproductIsCoproduct, Prod.fst, CategoryTheory.Limits.Cofan.mk, CategoryTheory.Limits.Sigma.desc, Prod.snd
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3 :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
e_4 :
  sigmaObj.{u_1, v, u} X =
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor X)
      (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
h :
  ∀ (x : C) (x_1 : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ x) (b : ι × ι'),
    CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b) (Sigma.desc x_1) =
      CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b)
        (Cofan.IsColimit.desc
          (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) x_1)
⊢ Eq (α :=
    {P : C} →
      (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
        (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
    (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) ⋯)
    (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3 :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
e_4 :
  sigmaObj.{u_1, v, u} X =
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor X)
      (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)
x : C
x_1 : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ x
b : ι × ι'
⊢ CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b) (Sigma.desc x_1) =
    CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b)
      (Cofan.IsColimit.desc (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        x_1)

Tactic:
simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Limits.coproductIsCoproduct