-- 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 (α :=
    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 })
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.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 })
⊢ 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:
ext ⟨⟨⟩⟩