-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : 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))
have 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))
Tactic: dsimp [homEquiv]