-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x : C
dsimp :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
        C))
    (CategoryStruct.comp (Y :=
        ComposableArrows.left.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)))
        (𝟙
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0)))
        (ComposableArrows.hom
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
                (a : ComposableArrows C 0) → ComposableArrows C 1)
              ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)) ≫
          𝟙
            (ComposableArrows.right.{v, u} (n := 1)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
                  (a : ComposableArrows C 0) → ComposableArrows C 1)
                ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)))) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C))
    (𝟙
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0)) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
        C))
    ((homEquiv :
          (a :
              Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x)
                ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x)) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x) ⟶
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x))
        (Edge.id ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C))
    (𝟙
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0)) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0) :
          C))

Tactic:
dsimp [homEquiv]

Premises used: CategoryTheory.nerve.homEquiv