awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j_1 : Fin (n + 1)
j : Fin n
⊢ Eq (α := F.obj { as := j.succ : Discrete (Fin (n + 1)) } ⟶ c₂.pt)
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })
        (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F.obj { as := j.succ }) j)
        (CategoryStruct.comp (Y := c₁.pt)
          (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b :
            (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₁.pt)
          (c₂.ι.app { as := WalkingPair.right } :
            obj.{0, v, 0, u} (pair (f 0) c₁.pt) { as := WalkingPair.right : Discrete WalkingPair } ⟶
              obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c₂.pt)
                { as := WalkingPair.right : Discrete WalkingPair })) :
      F.obj { as := j.succ : Discrete (Fin (n + 1)) } ⟶ c₂.pt)
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })
        (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F.obj { as := j.succ }) j)
        ((Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ i) :
      F.obj { as := j.succ : Discrete (Fin (n + 1)) } ⟶ c₂.pt)

Tactic:
simpa only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app,
        Category.assoc, extendCofan_pt, Functor.const_obj_obj, NatTrans.comp_app, extendCofan_ι_app,
        Fin.cases_succ, Functor.const_map_app] using congr_app e ⟨j.succ⟩

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Discrete.functor_obj, Fin.succ, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Discrete.mk, CategoryTheory.extendCofan_pt, CategoryTheory.Functor.const_map_app, CategoryTheory.extendCofan_ι_app, CategoryTheory.Limits.colimit.ι_desc_assoc, Fin.cases_succ, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
h_obj : ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X
h_map :
  ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y),
    HEq (F.map f) (β := obj.{0, v, 0, u} (Discrete.functor F') X ⟶ obj.{0, v, 0, u} (Discrete.functor F') Y)
      (map (Discrete.functor F') f)
⊢ F = Discrete.functor F'

Tactic:
apply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X

Tactic:
fun i ↦ rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X

Tactic:
exact fun i ↦ rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i_1 : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i_1
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
i : Fin (n + 1)
⊢ HEq
    (F.map
      {
        down :=
          { down := ⋯ : PLift ({ as := i : Discrete (Fin (n + 1)) }.as = { as := i : Discrete (Fin (n + 1)) }.as) } :
        ULift.{0, 0} (PLift ({ as := i : Discrete (Fin (n + 1)) }.as = { as := i : Discrete (Fin (n + 1)) }.as)) })
    (β :=
    obj.{0, v, 0, u} (Discrete.functor F') { as := i : Discrete (Fin (n + 1)) } ⟶
      obj.{0, v, 0, u} (Discrete.functor F') { as := i : Discrete (Fin (n + 1)) })
    (map (Discrete.functor F') { down := { down := ⋯ } })

Tactic:
simp [F']
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ F = Discrete.functor F'

Tactic:
have : F = Discrete.functor F' := by
      apply Functor.hext
      · exact fun i ↦ rfl
      · rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
        simp [F']
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
refine_2 :
  (F' : Fin (n + 1) → C) →
    (this : F = Discrete.functor F') →
      IsColimit (F := pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }))
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }))
⊢ IsColimit (F := pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }))
    (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
      (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }))

Tactic:
clear_value F'
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
⊢ CategoryStruct.comp (Y :=
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt (F :=
            pair (F' 0)
              (sigmaObj.{0, v, u} fun (j : Fin n) ↦
                obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) }))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
      (Hc.desc
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦
              Sigma.ι.{0, v, u} (C := C)
                  (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                  i ≫
                f₂)
            i)) =
    f₁

Tactic:
simp only [Discrete.functor_obj, pair_obj_left, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inl, IsColimit.fac, Cofan.mk_pt, Cofan.mk_ι_app,
        Fin.cases_zero]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Discrete.functor_obj, Fin.cases_zero, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
refine_2 :
  CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
      (Hc.desc
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)) =
    f₂
⊢ CategoryStruct.comp (Y :=
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt (F :=
            pair (F' 0)
              (sigmaObj.{0, v, u} fun (j : Fin n) ↦
                obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) }))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
      (Hc.desc
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦
              Sigma.ι.{0, v, u} (C := C)
                  (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                  i ≫
                f₂)
            i)) =
    f₂

Tactic:
simp only [Discrete.functor_obj, pair_obj_right, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inr]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
refine_2 :
  ∀ (j : Fin n),
    CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (j : Fin n) ↦ F' j.succ)
        (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) j)
        (CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
          (Hc.desc
            (Cofan.mk T fun (i : Fin (n + 1)) ↦
              Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
                (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i))) =
      Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) j ≫ f₂
⊢ CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
      (Hc.desc
        (Cofan.mk T fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
            (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)) =
    f₂

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j_1 : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
j : Fin n
⊢ CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (j : Fin n) ↦ F' j.succ)
      (Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) j)
      (CategoryStruct.comp (Y := c.pt) (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })
        (Hc.desc
          (Cofan.mk T fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
              (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i))) =
    Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) j ≫ f₂

Tactic:
simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt,
        Cofan.mk_ι_app, IsColimit.fac, Fin.cases_succ]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc_assoc, Fin.cases_succ
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ :
  BinaryCofan.inl
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })) ≫
      f₃ =
    f₁
m₂ :
  BinaryCofan.inr
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })) ≫
      f₃ =
    f₂
refine_2 :
  f₃ =
    Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)
⊢ f₃ =
    Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦
            Sigma.ι.{0, v, u} (C := C)
                (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) i ≫
              f₂)
          i)

Tactic:
simp only [Discrete.functor_obj_eq_as, pair_obj_left, BinaryCofan.mk_pt, const_obj_obj,
        BinaryCofan.mk_inl, pair_obj_right, BinaryCofan.mk_inr] at m₁ m₂ ⊢

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
⊢ f₃ =
    Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)

Tactic:
Hc.uniq (Cofan.mk T (Fin.cases f₁
        (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))) _ ?_

Premises used: Fin.succ, CategoryTheory.Limits.IsColimit.uniq, Fin.cases, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst_2 : HasFiniteCoproducts.{v, u} C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor F')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C) (Discrete.functor F') (Discrete.functor f)
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ :
  (sigmaObj.{0, v, u} fun (j : Fin n) ↦
      obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }) ⟶
    T
f₃ :
  Cocone.pt (F :=
      pair (F' 0)
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) }))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ : Discrete (Fin (n + 1)) })) ⟶
    T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
refine_2 :
  ∀ (j : Discrete (Fin (n + 1))),
    c.ι.app j ≫ f₃ =
      NatTrans.app
        (Cocone.ι
          (Cofan.mk T fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
              (fun (i : Fin n) ↦
                Sigma.ι.{0, v, u} (C := C)
                    (fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
                    i ≫
                  f₂)
              i))
        j
⊢ f₃ =
    Hc.desc
      (Cofan.mk T fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ T) f₁
          (fun (i : Fin n) ↦ Sigma.ι.{0, v, u} (C := C) (fun (j : Fin n) ↦ F' j.succ) i ≫ f₂) i)

Tactic:
refine Hc.uniq (Cofan.mk T (Fin.cases f₁
        (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))) _ ?_

Premises used: CategoryTheory.Limits.IsColimit.uniq, Fin.cases, CategoryTheory.Limits.Cofan.mk