-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
⊢ Eq.{v + 1} (α :=
    (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
        (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
          Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
        fun (x : Fin ((Opposite.unop m).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
      piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (fun (x : Fin ((Opposite.unop n).len + 1)) ↦
            Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          fun (x : Fin ((Opposite.unop n).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
        (WidePullback.lift
            (WidePullback.base fun (x : Fin ((Opposite.unop m).len + 1)) ↦
              Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
            (fun (i : Fin ((Opposite.unop n).len + 1)) ↦
              WidePullback.π
                (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                  Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                ((SimplexCategory.Hom.toOrderHom f.unop :
                    (a : Fin ((Opposite.unop n).len + 1)) → Fin ((Opposite.unop m).len + 1))
                  i))
            ⋯ :
          (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              fun (x : Fin ((Opposite.unop m).len + 1)) ↦
              Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
            widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              (fun (x : Fin ((Opposite.unop n).len + 1)) ↦
                Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              fun (x : Fin ((Opposite.unop n).len + 1)) ↦
              Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
        (Iso.hom
            (wideCospan.limitIsoPi (Fin ((Opposite.unop n).len + 1))
              (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))) :
          (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              (fun (x : Fin ((Opposite.unop n).len + 1)) ↦
                Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              fun (x : Fin ((Opposite.unop n).len + 1)) ↦
              Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
            piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X) :
      (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
            Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          fun (x : Fin ((Opposite.unop m).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
        piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)
    (CategoryStruct.comp (Y := piObj.{0, v, u} fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
        (Iso.hom
            (wideCospan.limitIsoPi (Fin ((Opposite.unop m).len + 1))
              (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))) :
          (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              fun (x : Fin ((Opposite.unop m).len + 1)) ↦
              Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
            piObj.{0, v, u} fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
        (Pi.lift fun (i : Fin ((Opposite.unop n).len + 1)) ↦
            Pi.π (fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
              ((SimplexCategory.Hom.toOrderHom f.unop :
                  (a : Fin ((Opposite.unop n).len + 1)) → Fin ((Opposite.unop m).len + 1))
                i) :
          Quiver.Hom.{v, u} (V := C) (piObj.{0, v, u} fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
            (piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)) :
      (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
            Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          fun (x : Fin ((Opposite.unop m).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
        piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)
have h : ∀ (j : ℕ) (isLt : j < (Opposite.unop n).len + 1),
  Eq.{v + 1} (α :=
    (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
        (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
          Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
        fun (x : Fin ((Opposite.unop m).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
      X)
    (CategoryStruct.comp (Y := piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
            (fun (x : Fin ((Opposite.unop n).len + 1)) ↦
              Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
            fun (x : Fin ((Opposite.unop n).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (WidePullback.lift
              (WidePullback.base fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
              (fun (i : Fin ((Opposite.unop n).len + 1)) ↦
                WidePullback.π
                  (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                    Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                  ((SimplexCategory.Hom.toOrderHom f.unop :
                      (a : Fin ((Opposite.unop n).len + 1)) → Fin ((Opposite.unop m).len + 1))
                    i))
              sorry :
            (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                  Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
              widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                (fun (x : Fin ((Opposite.unop n).len + 1)) ↦
                  Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                fun (x : Fin ((Opposite.unop n).len + 1)) ↦
                Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (Iso.hom
              (wideCospan.limitIsoPi (Fin ((Opposite.unop n).len + 1))
                (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))) :
            (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                (fun (x : Fin ((Opposite.unop n).len + 1)) ↦
                  Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                fun (x : Fin ((Opposite.unop n).len + 1)) ↦
                Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
              piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X))
        (Pi.π (fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X) ⟨j, isLt⟩) :
      (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
            Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          fun (x : Fin ((Opposite.unop m).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
        X)
    (CategoryStruct.comp (Y := piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)
        (CategoryStruct.comp (Y := piObj.{0, v, u} fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
          (Iso.hom
              (wideCospan.limitIsoPi (Fin ((Opposite.unop m).len + 1))
                (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))) :
            (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                  Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
                fun (x : Fin ((Opposite.unop m).len + 1)) ↦
                Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
              piObj.{0, v, u} fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
          (Pi.lift fun (i : Fin ((Opposite.unop n).len + 1)) ↦
              Pi.π (fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
                ((SimplexCategory.Hom.toOrderHom f.unop :
                    (a : Fin ((Opposite.unop n).len + 1)) → Fin ((Opposite.unop m).len + 1))
                  i) :
            Quiver.Hom.{v, u} (V := C) (piObj.{0, v, u} fun (x : Fin ((Opposite.unop m).len + 1)) ↦ X)
              (piObj.{0, v, u} fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X)))
        (Pi.π (fun (x : Fin ((Opposite.unop n).len + 1)) ↦ X) ⟨j, isLt⟩) :
      (widePullback.{0, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          (fun (x : Fin ((Opposite.unop m).len + 1)) ↦
            Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
          fun (x : Fin ((Opposite.unop m).len + 1)) ↦ Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) ⟶
        X)
Tactic: ext ⟨j⟩