-- 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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : (edgeMk f).CompStruct (edgeMk g) (edgeMk (f ≫ g))
⊢ 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) Z :
                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) Z))) →
            (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) Z)))
        ((edgeMk (f ≫ g)).toTruncated.map φ) :
      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) Z :
                  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))
    (CategoryStruct.comp (Y :=
        (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) Y :
                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)))))
        ((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) Y))) →
              (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) Y)))
          ((edgeMk f).toTruncated.map φ))
        ((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) Y))
                  ((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) Z))) →
              (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) Y)) ⟶
                (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) Z)))
          ((edgeMk g).toTruncated.map φ)) :
      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) Z :
                  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:
exact (nerve.homEquiv_comp (h.toTruncated.map φ)).symm

Premises used: SSet.Truncated.Edge.CompStruct.map, SSet.Edge.CompStruct.toTruncated, CategoryTheory.nerve.homEquiv_comp, Eq.symm