-- 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₁ : 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_4 :
  ∀
    (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 }) ⋯))),
    Nonempty (IsColimit c)
refine_1 :
  ∀ (j : Fin n), (α.app { as := j.succ : Discrete (Fin (n + 1)) } ≫ c₁.inj j) ≫ c₂.inr = c.ι.app { as := j.succ } ≫ i
refine_2 :
  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)))
⊢ Nonempty (IsColimit c)
have refine_3 : ∀ (j : Discrete (Fin n)),
  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)) }) sorry)))
      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 }) sorry))
      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: have t₁' := @t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩))
    (Cofan.mk (pullback c₂.inr i) fun j ↦ pullback.lift (α.app _ ≫ c₁.inj _) (c.ι.app _) ?_)
    (Discrete.natTrans fun i ↦ α.app _) (pullback.fst _ _) ?_ (.of_discrete _) ?_