-- 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
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)
j : Fin n
h :
  IsPullback (P := F.obj { as := j.castSucc }) (c.ι.app { as := j.castSucc }) (α.app { as := j.castSucc }) i
    ((extendCofan c₁ c₂).ι.app { as := j.castSucc })
refine_3 :
  ∀
    (t₁' :
      IsPullback (P :=
        obj.{0, v, 0, u} (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ }) { as := j : Discrete (Fin n) })
        (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 })
              (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
                (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ }))))
          { as := j : Discrete (Fin n) })
        (NatTrans.app
          (Cocone.ι
            (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
              (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ })))
          { as := j })
        (NatTrans.app (Discrete.natTrans fun (i : Discrete (Fin n)) ↦ α.app { as := i.as.succ }) { as := j })
        (Sigma.desc fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j) (c₁.ι.app { as := j : Discrete (Fin n) })),
    IsPullback (P := F.obj { as := j.succ }) (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i
      ((extendCofan c₁ c₂).ι.app { as := j.succ })
⊢ IsPullback (P := F.obj { as := j.succ }) (c.ι.app { as := j.succ }) (α.app { as := j.succ }) i
    ((extendCofan c₁ c₂).ι.app { as := j.succ })
have refine_3₁ : 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 })
        (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
          (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ }))))
    (Cocone.ι
      (Cofan.mk (colimit.cocone (Discrete.functor fun (j : Fin n) ↦ F.obj { as := j.succ })).1
        (Sigma.ι fun (j : Fin n) ↦ F.obj { as := j.succ })))
    (map (const (Discrete (Fin n))) (Sigma.desc fun (j : Fin n) ↦ α.app { as := j.succ } ≫ c₁.inj j)))
Tactic: have t₁' := (@t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩)) (Cofan.mk _ _) (Discrete.natTrans
      fun i ↦ α.app _) (Sigma.desc (fun j ↦ α.app _ ≫ c₁.inj _)) ?_
      (.of_discrete _)).mp ⟨coproductIsCoproduct _⟩ ⟨j⟩