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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair (F.obj { as := 0 : Discrete (Fin (n + 1)) }) (pullback c₂.inr i))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c₂.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι) { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt (F := pair (F.obj { as := 0 : Discrete (Fin (n + 1)) }) (pullback c₂.inr i))
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))))
        (Cocone.ι (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i)))
        (map (const (Discrete WalkingPair)) i))
      { as := WalkingPair.left })

Tactic:
simpa [mapPair] using congr_app e ⟨0⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.mapPair, OfNat.ofNat, 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair (F.obj { as := 0 : Discrete (Fin (n + 1)) }) (pullback c₂.inr i))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c₂.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι) { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt (F := pair (F.obj { as := 0 : Discrete (Fin (n + 1)) }) (pullback c₂.inr i))
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))))
        (Cocone.ι (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i)))
        (map (const (Discrete WalkingPair)) i))
      { as := WalkingPair.right })

Tactic:
simpa using pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
refine_4 : IsPullback (c.ι.app { as := 0 }) (α.app { as := 0 : Discrete (Fin (n + 1)) }) i c₂.inl
⊢ IsPullback (P :=
    obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (pullback c₂.inr i)) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i)))
      { as := WalkingPair.left })
    (NatTrans.app (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)) { as := WalkingPair.left }) i
    (c₂.ι.app { as := WalkingPair.left })

Tactic:
simp only [pair_obj_right, Functor.const_obj_obj, pair_obj_left, BinaryCofan.mk_pt,
        BinaryCofan.ι_app_left, BinaryCofan.mk_inl, mapPair_left]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Limits.BinaryCofan.ι_app_left, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.mapPair_left
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback (c.ι.app { as := 0 }) (α.app { as := 0 : Discrete (Fin (n + 1)) }) i c₂.inl

Tactic:
H ⟨0⟩

Premises used: Eq.mpr, CategoryTheory.Discrete.functor, Fin.induction.go, Fin.ofNat, CategoryTheory.Discrete.mk, Fin.induction, CategoryTheory.Limits.pair, Nat.mod, Fin.cases, OfNat.ofNat
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback (c.ι.app { as := 0 }) (α.app { as := 0 : Discrete (Fin (n + 1)) }) i c₂.inl

Tactic:
exact H ⟨0⟩

Premises used: CategoryTheory.Discrete.mk, OfNat.ofNat
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
refine_4 : IsPullback (P := pullback c₂.inr i) (pullback.snd c₂.inr i) (pullback.fst c₂.inr i) i c₂.inr
⊢ IsPullback (P :=
    obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (pullback c₂.inr i)) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i)))
      { as := WalkingPair.right })
    (NatTrans.app (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)) { as := WalkingPair.right }) i
    (c₂.ι.app { as := WalkingPair.right })

Tactic:
simp only [pair_obj_right, Functor.const_obj_obj, BinaryCofan.mk_pt, BinaryCofan.ι_app_right,
        BinaryCofan.mk_inr, mapPair_right]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.BinaryCofan.ι_app_right, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.mapPair_right
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback (P := pullback c₂.inr i) (pullback.snd c₂.inr i) (pullback.fst c₂.inr i) i c₂.inr

Tactic:
(IsPullback.of_hasPullback (BinaryCofan.inr c₂) i).flip

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback (P := pullback c₂.inr i) (pullback.snd c₂.inr i) (pullback.fst c₂.inr i) i c₂.inr

Tactic:
exact (IsPullback.of_hasPullback (BinaryCofan.inr c₂) i).flip

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
t₂' :
  Nonempty
    (IsColimit (F := pair (F.obj { as := 0 }) (pullback c₂.inr i))
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i)))
refine_4 :
  ∀
    (H₂ :
      IsColimit (F := pair (F.obj { as := 0 }) (pullback c₂.inr i))
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))),
    Nonempty (IsColimit c)
⊢ Nonempty (IsColimit c)

Tactic:
obtain ⟨H₂⟩ := t₂'
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ :
  IsColimit (F := pair (F.obj { as := 0 }) (pullback c₂.inr i))
    (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))
refine_4 :
  ∀ (F' : Fin (n + 1) → C) (this : F = Discrete.functor F')
    (H₁ :
      IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
        (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
          pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
    (H₂ :
      IsColimit (F := pair (F.obj { as := 0 }) (pullback c₂.inr i))
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))),
    Nonempty (IsColimit c)
⊢ Nonempty (IsColimit c)

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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C
this : F = Discrete.functor F'
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ :
  IsColimit (F := pair (F.obj { as := 0 }) (pullback c₂.inr i))
    (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))
refine_4 :
  ∀ (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 α)
    (H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j))
    (H₁ :
      IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
        Discrete.functor fun (j : Fin n) ↦
          obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
        (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
          pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
    (H₂ :
      IsColimit (F := pair (obj.{0, v, 0, u} (Discrete.functor F') { as := 0 }) (pullback c₂.inr i))
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))),
    Nonempty (IsColimit c)
⊢ Nonempty (IsColimit c)

Tactic:
subst this
-- 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
    Discrete.functor fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ :
  IsColimit (F := pair (obj.{0, v, 0, u} (Discrete.functor F') { as := 0 }) (pullback c₂.inr i))
    (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))
⊢ Nonempty (IsColimit c)

Tactic:
⟨IsColimit.ofIsoColimit (extendCofanIsColimit
    (fun i ↦ (Discrete.functor F').obj ⟨i⟩) H₁ H₂) <| Cocone.ext (Iso.refl _) ?_⟩

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.extendCofanIsColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Discrete.functor, CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.Discrete.mk, CategoryTheory.Functor.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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
H₁ :
  IsColimit.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
    Discrete.functor fun (j : Fin n) ↦ obj.{0, v, 0, u} (Discrete.functor F') { as := j.succ : Discrete (Fin (n + 1)) })
    (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
H₂ :
  IsColimit (F := pair (obj.{0, v, 0, u} (Discrete.functor F') { as := 0 }) (pullback c₂.inr i))
    (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))
refine_4 :
  ∀ (j : Discrete (Fin (n + 1))),
    NatTrans.app
          (Cocone.ι
            (extendCofan
              (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
                pullback.lift (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j)
                  (c.ι.app { as := j.succ : Discrete (Fin (n + 1)) }) ⋯)
              (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))))
          j ≫
        Iso.hom
          (Iso.refl
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin (n + 1))) (F :=
              Discrete.functor fun (i : Fin (n + 1)) ↦
                obj.{0, v, 0, u} (Discrete.functor F') { as := i : Discrete (Fin (n + 1)) })
              (extendCofan
                (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
                  pullback.lift (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j)
                    (c.ι.app { as := j.succ : Discrete (Fin (n + 1)) }) ⋯)
                (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i))))) =
      c.ι.app j
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨IsColimit.ofIsoColimit (extendCofanIsColimit
    (fun i ↦ (Discrete.functor F').obj ⟨i⟩) H₁ H₂) <| Cocone.ext (Iso.refl _) ?_⟩