-- 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
dsimp :
  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)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Arrow.cechNerve (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) m ⟶
      Functor.obj.{0, v, 0, u} (cechNerveTerminalFrom X) n)
    (Functor.map (Arrow.cechNerve (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) f ≫
      Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (wideCospan.limitIsoPi (Fin ((Opposite.unop x).len + 1))
                (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) :
              limit.{0, 0, v, u} (J := WidePullbackShape (Fin ((Opposite.unop x).len + 1)))
                  (wideCospan (Fin ((Opposite.unop x).len + 1))
                    (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))) ≅
                piObj.{0, v, u} fun (x : Fin ((Opposite.unop x).len + 1)) ↦
                  Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))))
          n))
    (Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (wideCospan.limitIsoPi (Fin ((Opposite.unop x).len + 1))
                (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) :
              limit.{0, 0, v, u} (J := WidePullbackShape (Fin ((Opposite.unop x).len + 1)))
                  (wideCospan (Fin ((Opposite.unop x).len + 1))
                    (Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))) ≅
                piObj.{0, v, u} fun (x : Fin ((Opposite.unop x).len + 1)) ↦
                  Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))))
          m) ≫
      Functor.map (cechNerveTerminalFrom X) f)

Tactic:
dsimp only [cechNerveTerminalFrom, Arrow.cechNerve]

Premises used: CategoryTheory.cechNerveTerminalFrom, CategoryTheory.Arrow.cechNerve