-- Module: Mathlib.AlgebraicTopology.CechNerve
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
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))
              ⋯ :
            (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:
simp