-- 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))
dsimp :
  𝟙
        (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))
⊢ Eq (α :=
    Quiver.Hom (V := (↑(ReflQuiv.forget.obj Y) : Type u))
      (Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
            (a :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
          f))
      (Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((nerveFunctor₂.obj X).map (δ₂ 0 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
            (a :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
          f)))
    (Prefunctor.map
      (ReflPrefunctor.toPrefunctor
        ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
          Iso.hom
            ((fun (C : Cat.{u, u}) ↦
                (ofNerve₂ (↑C : Type u) :
                  ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅ ReflQuiv.of (↑C : Type u)))
              Y)))
      { edge := f, src_eq := ⋯, tgt_eq := ⋯ })
    (Eq.recOn (motive :=
      fun (x : (↑(ReflQuiv.forget.obj Y) : Type u))
        (x_1 :
          Prefunctor.obj (V := (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u))
              (ReflPrefunctor.toPrefunctor
                (Iso.hom
                    ((fun (C : Cat.{u, u}) ↦
                        (ofNerve₂ (↑C : Type u) :
                          ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                            ReflQuiv.of (↑C : Type u)))
                      X) ≫
                  ReflQuiv.forget.map F))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((nerveFunctor₂.obj X).map (δ₂ 0 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
                f) =
            x) ↦
      Prefunctor.obj
          (ReflPrefunctor.toPrefunctor
            ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
              Iso.hom
                ((fun (C : Cat.{u, u}) ↦
                    (ofNerve₂ (↑C : Type u) :
                      ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                        ReflQuiv.of (↑C : Type u)))
                  Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
            f) ⟶
        x)
      ⋯
      (Eq.recOn (motive :=
        fun (x : (↑(ReflQuiv.forget.obj Y) : Type u))
          (x_1 :
            Prefunctor.obj (V := (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u))
                (ReflPrefunctor.toPrefunctor
                  (Iso.hom
                      ((fun (C : Cat.{u, u}) ↦
                          (ofNerve₂ (↑C : Type u) :
                            ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                              ReflQuiv.of (↑C : Type u)))
                        X) ≫
                    ReflQuiv.forget.map F))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
                  f) =
              x) ↦
        x ⟶
          Prefunctor.obj (V := (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u))
            (ReflPrefunctor.toPrefunctor
              (Iso.hom
                  ((fun (C : Cat.{u, u}) ↦
                      (ofNerve₂ (↑C : Type u) :
                        ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                          ReflQuiv.of (↑C : Type u)))
                    X) ≫
                ReflQuiv.forget.map F))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((nerveFunctor₂.obj X).map (δ₂ 0 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
              f))
        ⋯
        (Prefunctor.map
          (ReflPrefunctor.toPrefunctor
            (Iso.hom
                ((fun (C : Cat.{u, u}) ↦
                    (ofNerve₂ (↑C : Type u) :
                      ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                        ReflQuiv.of (↑C : Type u)))
                  X) ≫
              ReflQuiv.forget.map F))
          { edge := f, src_eq := ⋯, tgt_eq := ⋯ })))

Tactic:
dsimp [ofNerve₂, ReflQuiv.isoOfEquiv, ReflQuiv.isoOfQuivIso,
        Quiv.isoOfEquiv, nerveHomEquiv_apply]

Premises used: CategoryTheory.ReflQuiv.isoOfEquiv, CategoryTheory.Quiv.isoOfEquiv, SSet.OneTruncation₂.nerveHomEquiv_apply, CategoryTheory.ReflQuiv.isoOfQuivIso, SSet.OneTruncation₂.ofNerve₂