-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ Eq (α :=
    Quiver.Hom (V := D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D))
    ((homEquiv :
          (a :
              SSet.Edge
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x))
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x))) →
            (nerveEquiv : (a : ComposableArrows D 0) → D)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x)) ⟶
              (nerveEquiv : (a : ComposableArrows D 0) → D)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x)))
        (SSet.Truncated.Edge.map (SSet.Edge.toTruncated (X := nerve C) (edgeMk (𝟙 x))) φ) :
      Quiver.Hom (V := D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D))
    (𝟙
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1))))) :
      Quiver.Hom (V := D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D))
have rw : Eq.{u + 1} (α :=
  Quiver.Hom (V := D)
    ((nerveEquiv : (a : ComposableArrows D 0) → D)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1))) :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
            ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
              ComposableArrows (↑(Cat.of C) : Type u) 0) :
          (fun (X : Type u) ↦ X)
            ((nerveFunctor₂.obj (Cat.of D)).obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  _root_._proof_1)))) :
      D)
    ((nerveEquiv : (a : ComposableArrows D 0) → D)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1))) :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
            ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
              ComposableArrows (↑(Cat.of C) : Type u) 0) :
          (fun (X : Type u) ↦ X)
            ((nerveFunctor₂.obj (Cat.of D)).obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  _root_._proof_1)))) :
      D))
  ((homEquiv :
        (a :
            SSet.Edge
              ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x))
              ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x))) →
          (nerveEquiv : (a : ComposableArrows D 0) → D)
              ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x)) ⟶
            (nerveEquiv : (a : ComposableArrows D 0) → D)
              ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x)))
      (SSet.Truncated.Edge.id
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (φ.app
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    SSet.Truncated.Edge._proof_1))) :
            (a :
                (fun (X : Type u) ↦ X)
                  (((SSet.truncation 2).obj (nerve C)).obj
                    (op { obj := ⦋0⦌, property := SSet.Truncated.Edge._proof_1 }))) →
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := SSet.Truncated.Edge._proof_1 })))
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows C 0))) :
    Quiver.Hom (V := D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D))
  (𝟙
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1))) :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
            ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
              ComposableArrows (↑(Cat.of C) : Type u) 0) :
          (fun (X : Type u) ↦ X)
            ((nerveFunctor₂.obj (Cat.of D)).obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  _root_._proof_1))))) :
    Quiver.Hom (V := D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) x :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D))
Tactic: rw [edgeMk_id, SSet.Edge.toTruncated_id, SSet.Truncated.Edge.map_id]