-- 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} (α :=
    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)
have 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))
          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) :
    (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: dsimp only [cechNerveTerminalFrom, Arrow.cechNerve]