awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
⊢ CategoryStruct.comp (Y := coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
      coprod.inl
      (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} f)
        (coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)))
        (Sigma.desc fun (j : ι) ↦
          if h : j = i then eqToHom ⋯ ≫ coprod.inl
          else
            Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
                (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
              coprod.inr)) =
    coprod.inl ≫ 𝟙 (coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
j : (↑{i}ᶜ : Type u_1)
h₂ :
  Eq.{v + 1} (α := f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (if h : (↑j : ι) = i then eqToHom ⋯ ≫ coprod.inl
      else
        Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
            (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) (↑j : ι) ⋯) ≫
          coprod.inr :
      f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫ coprod.inr :
      f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
⊢ CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
      (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j)
      (CategoryStruct.comp (Y := coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
        coprod.inr
        (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} f)
          (coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)))
          (Sigma.desc fun (j : ι) ↦
            if h : j = i then eqToHom ⋯ ≫ coprod.inl
            else
              Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
                coprod.inr))) =
    Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫
      coprod.inr ≫ 𝟙 (coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))

Tactic:
simp only [coprod.desc_comp, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
          eqToHom_refl, Category.id_comp, dite_true, BinaryCofan.mk_pt, BinaryCofan.ι_app_right,
          BinaryCofan.mk_inr, colimit.ι_desc_assoc, Discrete.functor_obj, Category.comp_id]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.eqToHom_refl, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.BinaryCofan.ι_app_right, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc, dite_true, CategoryTheory.Limits.coprod.desc_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
j : (↑{i}ᶜ : Type u_1)
⊢ Eq.{v + 1} (α := f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (if h : (↑j : ι) = i then eqToHom ⋯ ≫ coprod.inl
      else
        Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
            (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) (↑j : ι) ⋯) ≫
          coprod.inr :
      f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫ coprod.inr :
      f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))

Tactic:
dif_neg j.prop

Premises used: Set.Mem, setOf, dif_neg, Subtype.prop, Set.singleton
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
j : (↑{i}ᶜ : Type u_1)
⊢ Eq.{v + 1} (α := f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (if h : (↑j : ι) = i then eqToHom ⋯ ≫ coprod.inl
      else
        Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
            (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) (↑j : ι) ⋯) ≫
          coprod.inr :
      f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) j ≫ coprod.inr :
      f (↑j : ι) ⟶ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))

Tactic:
exact dif_neg j.prop

Premises used: dif_neg, Subtype.prop
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
simp :
  CategoryStruct.comp (Y :=
      Cocone.pt.{u_1, v, u_1, u} (F := Discrete.functor f)
        (ColimitCocone.cocone (getColimitCocone (Discrete.functor f))))
      (Sigma.ι f i)
      (Iso.inv (hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))))) =
    c.ι.app { as := i }
⊢ coprod.inl ≫ e'.inv = c.ι.app { as := i }

Tactic:
simp only [e, e', Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt,
      BinaryCofan.ι_app_left, BinaryCofan.mk_inl]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.BinaryCofan.ι_app_left, CategoryTheory.Limits.coprod.desc_comp, CategoryTheory.Iso.trans_inv
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{u_1, v, u_1, u} (F := Discrete.functor f)
        (ColimitCocone.cocone (getColimitCocone (Discrete.functor f))))
      (Sigma.ι f i)
      (Iso.inv (hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))))) =
    c.ι.app { as := i }

Tactic:
colimit.comp_coconePointUniqueUpToIso_inv _ _

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{u_1, v, u_1, u} (F := Discrete.functor f)
        (ColimitCocone.cocone (getColimitCocone (Discrete.functor f))))
      (Sigma.ι f i)
      (Iso.inv (hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))))) =
    c.ι.app { as := i }

Tactic:
exact colimit.comp_coconePointUniqueUpToIso_inv _ _

Premises used: CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
⊢ coprod.inl ≫ e'.inv = c.ι.app { as := i }

Tactic:
have : coprod.inl ≫ e'.inv = c.ι.app ⟨i⟩ := by
    simp only [e, e', Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt,
      BinaryCofan.ι_app_left, BinaryCofan.mk_inl]
    exact colimit.comp_coconePointUniqueUpToIso_inv _ _
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  hc.coconePointUniqueUpToIso (ColimitCocone.isColimit (getColimitCocone (Discrete.functor f))) ≪≫ e
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
clear_value :
  ∀ (e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)))
    (this : coprod.inl ≫ e'.inv = c.ι.app { as := i }), HasPullback g (c.ι.app { as := i : Discrete ι })
⊢ HasPullback g (c.ι.app { as := i : Discrete ι })

Tactic:
clear_value e'
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
rw : HasPullback g (coprod.inl ≫ e'.inv)
⊢ HasPullback g (c.ι.app { as := i : Discrete ι })

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ 𝟙 X ≫ g = (g ≫ e'.hom) ≫ e'.inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ IsPullback (𝟙 X) (g ≫ e'.hom) g e'.inv

Tactic:
have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this_1 : coprod.inl ≫ e'.inv = c.ι.app { as := i }
this : IsPullback (𝟙 X) (g ≫ e'.hom) g e'.inv
⊢ HasPullback g (coprod.inl ≫ e'.inv)

Tactic:
⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩

Premises used: CategoryTheory.Limits.coprod.inl, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Iso.hom, CategoryTheory.IsPullback.paste_horiz, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : C
f : ι → C
c : Cofan.{u_1, v, u} f
hc : IsColimit c
i : ι
g : X ⟶ Functor.obj.{u_1, v, u_1, u} (Functor.obj (Functor.const (Discrete ι)) c.pt) { as := i : Discrete ι }
e : sigmaObj.{u_1, v, u} f ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι)) :=
  {
    hom :=
      Sigma.desc fun (j : ι) ↦
        if h : j = i then eqToHom ⋯ ≫ coprod.inl
        else
          Sigma.ι.{u_1, v, u} (C := C) (fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
              (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i}ᶜ x) j h) ≫
            coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun (j : (↑{i}ᶜ : Type u_1)) ↦ Sigma.ι f (↑j : ι)), hom_inv_id := ⋯,
    inv_hom_id := ⋯ }
e' : c.pt ≅ coprod.{v, u} (f i) (sigmaObj.{u_1, v, u} fun (j : (↑{i}ᶜ : Type u_1)) ↦ f (↑j : ι))
this_1 : coprod.inl ≫ e'.inv = c.ι.app { as := i }
this : IsPullback (𝟙 X) (g ≫ e'.hom) g e'.inv
⊢ HasPullback g (coprod.inl ≫ e'.inv)

Tactic:
exact ⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i : Discrete ι
⊢ Mono (c.ι.app i)

Tactic:
mono_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) _

Premises used: CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts, CategoryTheory.mono_of_cofan_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_1 Y : C
inst_3 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_4 : Finite ι
X : ι → C
i : ι
⊢ Mono.{v, u} (Y := sigmaObj.{u_1, v, u} X) (Sigma.ι X i)

Tactic:
FinitaryExtensive.mono_ι (coproductIsCoproduct _) ⟨i⟩

Premises used: CategoryTheory.FinitaryExtensive.mono_ι, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.mk, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
F : Functor.{u_1, v, u_1, u} (Discrete ι) C
c : Cocone F
hc : IsColimit c
i j : Discrete ι
e : i ≠ j
⊢ IsPullback (P := initial.{v, u} C) (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

Tactic:
isPullback_initial_to_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) i j e

Premises used: CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen, CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
ι : Type u_1
inst_2 : Finite ι
X : ι → C
i j : ι
e : i ≠ j
⊢ IsPullback.{v, u} (P := initial.{v, u} C) (Z := sigmaObj.{u_1, v, u} X) (initial.to (X i)) (initial.to (X j))
    (Sigma.ι X i) (Sigma.ι X j)

Tactic:
FinitaryExtensive.isPullback_initial_to (coproductIsCoproduct _) ⟨i⟩ ⟨j⟩
    (ne_of_apply_ne Discrete.as e)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.colimit, ne_of_apply_ne, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.mk, CategoryTheory.Discrete.as, CategoryTheory.FinitaryExtensive.isPullback_initial_to, CategoryTheory.Limits.colimit.ι
-- 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
⊢ CoproductDisjoint.{v, u, u_1} X

Tactic:
⟨fun {c} hc i j e s hs ↦ ?_, fun hc i ↦ FinitaryExtensive.mono_ι hc ⟨i⟩⟩

Premises used: CategoryTheory.FinitaryExtensive.mono_ι, CategoryTheory.Discrete.mk, CategoryTheory.Limits.CoproductDisjoint.mk
-- 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
refine :
  ∀ {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)
⊢ CoproductDisjoint.{v, u, u_1} X

Tactic:
refine ⟨fun {c} hc i j e s hs ↦ ?_, fun hc i ↦ FinitaryExtensive.mono_ι hc ⟨i⟩⟩
-- 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
⊢ { as := i : Discrete ι } ≠ { as := j }

Tactic:
simpa