awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 α
⊢ Nonempty (IsColimit c) ↔
    ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
have refine : Nonempty (IsColimit c) →
  ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
Tactic: refine ⟨?_, isUniversalColimit_extendCofan f t₁.isUniversal t₂.isUniversal c α i e hα⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
have this : ∀ (j : Fin (n + 1)),
  IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
Tactic: ⟨j⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
have refine_3 : ∀
  (t₂' :
    ∀ (j : Discrete WalkingPair),
      IsPullback (P :=
        obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
        (NatTrans.app
          (Cocone.ι
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
          j)
        (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b)) j)
        i (c₂.ι.app j)),
  IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
Tactic: have t₂' := (@t₂ (pair (F.obj ⟨0⟩) (∐ fun (j : Fin n) ↦ F.obj ⟨j.succ⟩))
    (BinaryCofan.mk (P := c.pt) (c.ι.app _) (Sigma.desc fun b ↦ c.ι.app _))
    (mapPair (α.app _) (Sigma.desc fun b ↦ α.app _ ≫ c₁.inj _)) i ?_ (.of_discrete _)).mp ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
refine_3 :
  ∀
    (t₂' :
      ∀ (j : Discrete WalkingPair),
        IsPullback (P :=
          obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
          (NatTrans.app
            (Cocone.ι
              (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
                (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
            j)
          (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b))
            j)
          i (c₂.ι.app j)),
    IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
      ((extendCofan c₁ c₂).ι.app { as := j })
⊢ IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
have refine_1 : Eq (α :=
  Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C)
    (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }))
    (obj (const (Discrete WalkingPair)) c₂.pt))
  (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι)
  (CategoryStruct.comp (Y :=
    obj (const (Discrete WalkingPair))
      (Cocone.pt (F :=
        pair (F.obj { as := 0 : Discrete (Fin (n + 1)) })
          (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { 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)) }))))
    (Cocone.ι
      (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
        (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
    (map (const (Discrete WalkingPair)) i))
Tactic: have t₂' := (@t₂ (pair (F.obj ⟨0⟩) (∐ fun (j : Fin n) ↦ F.obj ⟨j.succ⟩))
    (BinaryCofan.mk (P := c.pt) (c.ι.app _) (Sigma.desc fun b ↦ c.ι.app _))
    (mapPair (α.app _) (Sigma.desc fun b ↦ α.app _ ≫ c₁.inj _)) i ?_ (.of_discrete _)).mp ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
refine_3 :
  ∀
    (t₂' :
      ∀ (j : Discrete WalkingPair),
        IsPullback (P :=
          obj.{0, v, 0, u} (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ })) j)
          (NatTrans.app
            (Cocone.ι
              (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
                (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
            j)
          (NatTrans.app (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b))
            j)
          i (c₂.ι.app j)),
    IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
      ((extendCofan c₁ c₂).ι.app { as := j })
refine_1 :
  Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C)
      (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }))
      (obj (const (Discrete WalkingPair)) c₂.pt))
    (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete WalkingPair))
        (Cocone.pt (F :=
          pair (F.obj { as := 0 : Discrete (Fin (n + 1)) })
            (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { 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)) }))))
      (Cocone.ι
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
      (map (const (Discrete WalkingPair)) i))
⊢ IsPullback (P := F.obj { as := j }) (c.ι.app { as := j }) (α.app { as := j }) i
    ((extendCofan c₁ c₂).ι.app { as := j })
have refine_2 : 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: have t₂' := (@t₂ (pair (F.obj ⟨0⟩) (∐ fun (j : Fin n) ↦ F.obj ⟨j.succ⟩))
    (BinaryCofan.mk (P := c.pt) (c.ι.app _) (Sigma.desc fun b ↦ c.ι.app _))
    (mapPair (α.app _) (Sigma.desc fun b ↦ α.app _ ≫ c₁.inj _)) i ?_ (.of_discrete _)).mp ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C)
      (pair (F.obj { as := 0 }) (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }))
      (obj (const (Discrete WalkingPair)) c₂.pt))
    (mapPair (α.app { as := 0 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete WalkingPair))
        (Cocone.pt (F :=
          pair (F.obj { as := 0 : Discrete (Fin (n + 1)) })
            (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { 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)) }))))
      (Cocone.ι
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
      (map (const (Discrete WalkingPair)) i))
have refine_1 : Eq (α :=
  obj.{0, v, 0, u}
      (pair (F.obj { as := 0 : Discrete (Fin (n + 1)) })
        (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ : Discrete (Fin (n + 1)) }))
      { 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 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ 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)) })
            (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { 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)) }))))
      (Cocone.ι
        (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
          (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
      (map (const (Discrete WalkingPair)) i))
    { as := WalkingPair.left })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Eq (α :=
    obj.{0, v, 0, u}
        (pair (F.obj { as := 0 : Discrete (Fin (n + 1)) })
          (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ : Discrete (Fin (n + 1)) }))
        { 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 }) (Sigma.desc fun (b : Fin n) ↦ α.app { as := b.succ } ≫ c₁.inj b) ≫ 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)) })
              (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { 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)) }))))
        (Cocone.ι
          (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
            (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })))
        (map (const (Discrete WalkingPair)) i))
      { as := WalkingPair.right })
have refine_1 : Eq (α := (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₂.pt)
  (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 }) :
    (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₂.pt)
  ((Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ i :
    (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₂.pt)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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)
⊢ Eq (α := (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₂.pt)
    (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 }) :
      (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₂.pt)
    ((Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ }) ≫ i :
      (sigmaObj.{0, v, u} fun (j : Fin n) ↦ F.obj { as := j.succ }) ⟶ c₂.pt)
have refine_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: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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'
have h_obj : ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ F = Discrete.functor F'
have 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)
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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
⊢ 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 }))
have this : 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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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'
⊢ 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 }))
have 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 }))
Tactic: clear_value F'
Cleared hypotheses: F', this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ IsColimit (F :=
    pair (obj.{0, v, 0, u} (Discrete.functor F') { as := 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 }))
have refine_2 : ∀ {T : C} (f : F' 0 ⟶ T)
  (g :
    (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 ≫
                g)
            i)) =
    f
Tactic: apply BinaryCofan.IsColimit.mk _ (fun {T} f₁ f₂ ↦ Hc.desc (Cofan.mk T (Fin.cases f₁
      (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))))