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' : 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))),
    Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
          (fun (i_1 : Fin n) ↦
            CategoryStruct.comp (Y := pullback c₂.inr i)
              (pullback.lift (α.app { as := i_1.succ } ≫ c₁.inj i_1) (c.ι.app { as := i_1.succ }) ⋯)
              (pullback.snd c₂.inr i))
          j.as ≫
        𝟙 c.pt =
      c.ι.app j
⊢ ∀ (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

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' : 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))
j : Fin (n + 1)
refine_4 :
  Eq.{v + 1} (α := F' j ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
        (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) j :
      F' j ⟶ c.pt)
    (c.ι.app { as := j } :
      obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := j : Discrete (Fin (n + 1)) } ⟶
        obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := j : Discrete (Fin (n + 1)) })
⊢ Eq.{v + 1} (α := F' { as := j : Discrete (Fin (n + 1)) }.as ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
          (fun (i_1 : Fin n) ↦
            CategoryStruct.comp (Y := pullback c₂.inr i)
              (pullback.lift (α.app { as := i_1.succ } ≫ c₁.inj i_1) (c.ι.app { as := i_1.succ }) ⋯)
              (pullback.snd c₂.inr i))
          { as := j : Discrete (Fin (n + 1)) }.as ≫
        𝟙 c.pt :
      F' { as := j : Discrete (Fin (n + 1)) }.as ⟶ c.pt)
    (c.ι.app { as := j } :
      obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := j : Discrete (Fin (n + 1)) } ⟶
        obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := j : Discrete (Fin (n + 1)) })

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt,
    PullbackCone.mk_π_app, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Category.comp_id, 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' : 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))
⊢ Eq.{v + 1} (α := F' 0 ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
        (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) 0 :
      F' 0 ⟶ c.pt)
    (c.ι.app { as := 0 } :
      obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := 0 } ⟶
        obj.{0, v, 0, u} (C := Discrete (Fin (n + 1))) (obj (const (Discrete (Fin (n + 1)))) c.pt)
          { as := 0 : Discrete (Fin (n + 1)) })

Tactic:
simp only [Fin.cases_zero]

Premises used: Fin.cases_zero
-- 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))
i_1 : Fin n
h :
  Eq.{v + 1} (α := F' i_1.castSucc ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
        (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) i_1.castSucc :
      F' i_1.castSucc ⟶ c.pt)
    (c.ι.app { as := i_1.castSucc } :
      obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := i_1.castSucc : Discrete (Fin (n + 1)) } ⟶
        obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := i_1.castSucc : Discrete (Fin (n + 1)) })
⊢ Eq.{v + 1} (α := F' i_1.succ ⟶ c.pt)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ F' x ⟶ c.pt) (c.ι.app { as := 0 })
        (fun (i : Fin n) ↦ c.ι.app { as := i.succ }) i_1.succ :
      F' i_1.succ ⟶ c.pt)
    (c.ι.app { as := i_1.succ } :
      obj.{0, v, 0, u} (Discrete.functor fun (i : Fin (n + 1)) ↦ F' i) { as := i_1.succ : Discrete (Fin (n + 1)) } ⟶
        obj.{0, v, 0, u} (obj (const (Discrete (Fin (n + 1)))) c.pt) { as := i_1.succ : Discrete (Fin (n + 1)) })

Tactic:
simp only [Fin.cases_succ]

Premises used: 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
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)

Tactic:
⟨?_, isUniversalColimit_extendCofan f t₁.isUniversal t₂.isUniversal c α i e hα⟩

Premises used: CategoryTheory.IsVanKampenColimit.isUniversal, Iff.intro, CategoryTheory.isUniversalColimit_extendCofan
-- 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 α
refine :
  Nonempty (IsColimit c) →
    ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
⊢ 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α⟩
-- 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
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 })
⊢ ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)

Tactic:
⟨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
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))
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 }))
⊢ 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 ⟨?_⟩
-- 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)
⊢ 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:
simpa only [pair_obj_left, Functor.const_obj_obj, pair_obj_right, Discrete.functor_obj,
        NatTrans.comp_app, mapPair_left, BinaryCofan.ι_app_left, BinaryCofan.mk_pt,
        BinaryCofan.mk_inl, Functor.const_map_app, extendCofan_pt,
        extendCofan_ι_app, Fin.cases_zero] using congr_app e ⟨0⟩

Premises used: CategoryTheory.Limits.BinaryCofan.mk_pt, CategoryTheory.Discrete.functor_obj, Fin.cases_zero, CategoryTheory.Limits.pair_obj_right, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Discrete.mk, CategoryTheory.extendCofan_pt, CategoryTheory.Functor.const_map_app, CategoryTheory.extendCofan_ι_app, CategoryTheory.Limits.BinaryCofan.ι_app_left, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, OfNat.ofNat, CategoryTheory.congr_app, 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₁ : 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_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)
⊢ 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 })

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₁ : 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_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)
⊢ 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:
ext j