-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : X ⟶ Functor.obj (truncation 2) (nerve C)
x :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := C)
      ((fun
            (x :
              X.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) :
                    (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                  x :
                (fun (X : Type u) ↦ X)
                  (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))) :
            C))
        x)
      ((fun
            (x :
              X.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) :
                    (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                  x :
                (fun (X : Type u) ↦ X)
                  (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))) :
            C))
        x))
    ((fun
          {x y :
            X.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))}
          (e : Edge x y) ↦
        ((nerve.homEquiv :
              (a :
                  SSet.Edge
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) :
                        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            (((truncation 2).obj (nerve C)).obj
                              (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                      x)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) :
                        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            (((truncation 2).obj (nerve C)).obj
                              (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                      y)) →
                (nerveEquiv : (a : ComposableArrows C 0) → C)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) :
                        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            (((truncation 2).obj (nerve C)).obj
                              (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                      x) ⟶
                  (nerveEquiv : (a : ComposableArrows C 0) → C)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) :
                        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            (((truncation 2).obj (nerve C)).obj
                              (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                      y))
            (e.map φ) :
          Quiver.Hom (V := C)
            ((nerveEquiv : (a : ComposableArrows C 0) → C)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (φ.app
                          (op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) :
                      (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                    x :
                  (fun (X : Type u) ↦ X)
                    (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1)))) :
              C)
            ((nerveEquiv : (a : ComposableArrows C 0) → C)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (φ.app
                          (op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) :
                      (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                    y :
                  (fun (X : Type u) ↦ X)
                    (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1)))) :
              C)))
      (Edge.id x))
    (𝟙
      ((fun
            (x :
              X.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) :
                    (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        (((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
                  x :
                (fun (X : Type u) ↦ X)
                  (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))) :
            C))
        x))

Tactic:
simpa using nerve.homEquiv_id (φ.app _ x)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.nerve.homEquiv_id, DFunLike.coe, CategoryTheory.NatTrans.app