-- 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
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))
                ⋯ :
              (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)
⊢ 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)

Tactic:
ext ⟨j⟩