-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
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.{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:
nerve.homEquiv_id _

Premises used: CategoryTheory.nerve.homEquiv_id