-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (X₀ :=
      F.obj
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
              (a : X.obj (op { obj := ⦋1⦌, property := Edge._proof_3 })) →
                X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _proof_2 _proof_5).op) :
                  (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) →
                    X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
                h.simplex :
              X.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))))
      (F.map
        (homMk
          (Edge.mk'
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _proof_2 _proof_5).op) :
                (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
              h.simplex)))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (X₀ :=
      F.obj
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
              (a : X.obj (op { obj := ⦋1⦌, property := Edge._proof_3 })) →
                X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_2 _proof_5).op) :
                  (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) →
                    X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
                h.simplex :
              X.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))))
      (F.map
        (homMk
          (Edge.mk'
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_2 _proof_5).op) :
                (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
              h.simplex)))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
this_1 : ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = y
this :
  ComposableArrows.mk₁ (F.map (homMk e₀₁) ≫ F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve C) 1) :
        (a : (fun (X : Type u) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (nerve C _⦋1⦌))
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))
rwa :
  ∀
    (this :
      ComposableArrows.mk₁ (F.map (homMk e₀₁ ≫ homMk e₁₂)) =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve C) 1) :
            (a : (fun (X : Type u) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (nerve C _⦋1⦌))
          (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₀₂.edge))) =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 _proof_2 _proof_5).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))
rwa₁ :
  ∀
    (this :
      ComposableArrows.mk₁ (F.map (homMk e₀₂)) =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve C) 1) :
            (a : (fun (X : Type u) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (nerve C _⦋1⦌))
          (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₀₂.edge))) =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 _proof_2 _proof_5).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₀₂.edge))) =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve C) 1) :
            (a : (fun (X : Type u) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (nerve C _⦋1⦌))
          (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₀₂.edge))) =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 _proof_2 _proof_5).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₀₂.edge))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))

Tactic:
rwa [← Functor.map_comp, homMk_comp_homMk h, ← h'] at this

Premises used: CategoryTheory.Functor.map_comp, SSet.Truncated.HomotopyCategory.homMk_comp_homMk