-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X Y : Cat
F : X ⟶ Y
f :
  (nerveFunctor₂.obj X).obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ Truncated.Edge._proof_2))
simp :
  ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((nerveFunctor₂.map F).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                  Truncated.Edge._proof_2))) :
          (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })) →
            ((truncation 2).obj (nerve (↑Y : Type u))).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 }))
        f) =
    F.toFunctor.map (ComposableArrows.hom f)
⊢ 𝟙
        (ComposableArrows.left (n := 0)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((nerveFunctor₂.map F).app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
              (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := _proof_1 })) →
                (nerveFunctor₂.obj Y).obj (op { obj := ⦋0⦌, property := _proof_1 }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                  (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_3 })) →
                    (nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))
                f :
              (nerveFunctor₂.obj X).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    Truncated.Edge._proof_1))))) ≫
      ComposableArrows.hom
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((nerveFunctor₂.map F).app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                      Truncated.Edge._proof_2))) :
              (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })) →
                ((truncation 2).obj (nerve (↑Y : Type u))).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 }))
            f) ≫
        𝟙
          (ComposableArrows.right (n := 1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((nerveFunctor₂.map F).app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                        Truncated.Edge._proof_2))) :
                (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })) →
                  ((truncation 2).obj (nerve (↑Y : Type u))).obj
                    (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 }))
              f)) =
    F.toFunctor.map
      (𝟙
          (ComposableArrows.left (n := 0)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_3 })) →
                  (nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))
              f)) ≫
        ComposableArrows.hom f ≫ 𝟙 (ComposableArrows.right f))

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp