-- 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
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
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
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.right : Discrete WalkingPair })
        (BinaryCofan.inr
          (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)) =
      g
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)
    (m :
      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)) })) ⟶
        T),
    BinaryCofan.inl
            (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
              (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })) ≫
          m =
        f →
      BinaryCofan.inr
              (BinaryCofan.mk (c.ι.app { as := 0 : Discrete (Fin (n + 1)) })
                (Sigma.desc fun (b : Fin n) ↦ c.ι.app { as := b.succ })) ≫
            m =
          g →
        m =
          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)
⊢ 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 }))

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₂))))

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.mk