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_1 : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i_1
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i_1 ((extendCofan c₁ c₂).ι.app j)
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₁ : 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
⊢ 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₁ : 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'
j : Fin n
⊢ (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j) ≫ c₂.inr = c.ι.app { as := j.succ } ≫ i

Tactic:
simpa only [Functor.const_obj_obj, pair_obj_right, Discrete.functor_obj, 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.pair_obj_right, CategoryTheory.Discrete.mk, CategoryTheory.extendCofan_pt, CategoryTheory.Functor.const_map_app, CategoryTheory.extendCofan_ι_app, 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₁ : 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'
refine_2 :
  ∀ (j : Discrete (Fin n)),
    Eq (α :=
      obj.{0, v, 0, u} (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) j ⟶
        obj.{0, v, 0, u} (obj (const (Discrete (Fin n))) c₁.pt) j)
      (NatTrans.app ((Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) ≫ c₁.ι) j)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          obj (const (Discrete (Fin n)))
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
              Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ : Discrete (Fin (n + 1)) })
              (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)) }) ⋯)))
          (Cocone.ι
            (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
              pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
          (map (const (Discrete (Fin n))) (pullback.fst c₂.inr i)))
        j)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete (Fin n)) C)
      (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) (obj (const (Discrete (Fin n))) c₁.pt))
    ((Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) ≫ c₁.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete (Fin n)))
        (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
          Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ : Discrete (Fin (n + 1)) })
          (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)) }) ⋯)))
      (Cocone.ι
        (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
          pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
      (map (const (Discrete (Fin n))) (pullback.fst c₂.inr i)))

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₁ : 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'
j : Discrete (Fin n)
refine_2 :
  α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app j =
    CategoryStruct.comp (Y := pullback c₂.inr i)
      (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
      (pullback.fst c₂.inr i)
⊢ Eq (α :=
    obj.{0, v, 0, u} (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) j ⟶
      obj.{0, v, 0, u} (obj (const (Discrete (Fin n))) c₁.pt) j)
    (NatTrans.app ((Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) ≫ c₁.ι) j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete (Fin n)))
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
            Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ : Discrete (Fin (n + 1)) })
            (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)) }) ⋯)))
        (Cocone.ι
          (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
            pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
        (map (const (Discrete (Fin n))) (pullback.fst c₂.inr i)))
      j)

Tactic:
dsimp
-- 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'
j : Discrete (Fin n)
⊢ α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app j =
    CategoryStruct.comp (Y := pullback c₂.inr i)
      (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
      (pullback.fst c₂.inr i)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Cofan.inj]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- 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'
j : Discrete (Fin n)
refine_3 :
  IsPullback (X := pullback c₂.inr i)
    (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
    (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) (pullback.fst c₂.inr i) (c₁.ι.app j)
⊢ IsPullback (P := obj.{0, v, 0, u} (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) j) (X :=
    obj.{0, v, 0, u}
      (obj (const (Discrete (Fin n)))
        (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
          Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ : Discrete (Fin (n + 1)) })
          (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)) }) ⋯)))
      j)
    (NatTrans.app
      (Cocone.ι
        (Cofan.mk (pullback c₂.inr i) fun (j : Fin n) ↦
          pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
      j)
    (NatTrans.app (Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) j) (pullback.fst c₂.inr i)
    (c₁.ι.app j)

Tactic:
simp only [pair_obj_right, Functor.const_obj_obj, Discrete.functor_obj,
      Cofan.mk_pt, Cofan.mk_ι_app, Discrete.natTrans_app]

Premises used: CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Discrete.natTrans_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'
j : Discrete (Fin n)
⊢ IsPullback (X := pullback c₂.inr i)
    (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
    (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) (pullback.fst c₂.inr i) (c₁.ι.app j)

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

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.of_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'
j : Discrete (Fin n)
refine_3 :
  IsPullback
    (CategoryStruct.comp (Y := pullback c₂.inr i)
      (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
      (pullback.snd c₂.inr i))
    (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) i (c₁.ι.app j ≫ c₂.inr)
refine_3₁ :
  CategoryStruct.comp (Y := pullback c₂.inr i)
      (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
      (pullback.fst c₂.inr i) =
    α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app j
⊢ IsPullback (X := pullback c₂.inr i)
    (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
    (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) (pullback.fst c₂.inr i) (c₁.ι.app j)

Tactic:
refine IsPullback.of_right ?_ ?_ (IsPullback.of_hasPullback (BinaryCofan.inr c₂) i).flip

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.of_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'
j : Discrete (Fin n)
refine_3 :
  IsPullback (c.ι.app { as := j.as.succ }) (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) i (c₁.ι.app j ≫ c₂.inr)
⊢ IsPullback
    (CategoryStruct.comp (Y := pullback c₂.inr i)
      (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
      (pullback.snd c₂.inr i))
    (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) i (c₁.ι.app j ≫ c₂.inr)

Tactic:
simp only [Functor.const_obj_obj, pair_obj_right, limit.lift_π,
        PullbackCone.mk_pt, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.limit.lift_π
-- 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'
j : Discrete (Fin n)
⊢ IsPullback (c.ι.app { as := j.as.succ }) (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) i (c₁.ι.app j ≫ c₂.inr)

Tactic:
H _

Premises used: Fin.succ, CategoryTheory.Discrete.functor, Fin.induction.go, Fin.induction, CategoryTheory.Limits.pair, Fin.cases
-- 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'
j : Discrete (Fin n)
⊢ IsPullback (c.ι.app { as := j.as.succ }) (α.app { as := j.as.succ : Discrete (Fin (n + 1)) }) i (c₁.ι.app j ≫ c₂.inr)

Tactic:
exact H _
-- 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'
j : Discrete (Fin n)
⊢ CategoryStruct.comp (Y := pullback c₂.inr i)
      (pullback.lift (α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯)
      (pullback.fst c₂.inr i) =
    α.app { as := j.as.succ : Discrete (Fin (n + 1)) } ≫ c₁.ι.app j

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Cofan.inj]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- 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'
t₁' :
  Nonempty
    (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 :
  ∀
    (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 }) ⋯)),
    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 }) ⋯)
refine_4 :
  ∀
    (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)))),
    Nonempty (IsColimit c)
refine_4₁ :
  Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair (F.obj { as := 0 }) (pullback c₂.inr i))
      (obj (const (Discrete WalkingPair)) c₂.pt))
    (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι)
    (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))
refine_4₂ :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P := obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (pullback c₂.inr i)) j)
      (NatTrans.app (Cocone.ι (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) }) (pullback.snd c₂.inr i)))
        j)
      (NatTrans.app (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)) j) i (c₂.ι.app j)
⊢ Nonempty (IsColimit c)

Tactic:
have t₂' := @t₂ (pair (F.obj ⟨0⟩) (pullback c₂.inr i))
    (BinaryCofan.mk (c.ι.app ⟨0⟩) (pullback.snd _ _)) (mapPair (α.app _) (pullback.fst _ _)) i ?_
    (.of_discrete _) ?_