-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
dsimp :
  Eq (α :=
    Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((homToNerveMk (F ⋙ G)).app
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge :
      Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (CategoryTheory.Functor.map (truncation 2) (nerveMap G))
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((homToNerveMk F).app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
            f.edge :
          Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
      Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((homToNerveMk (F ⋙ G)).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f.edge :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ)
          (Functor.obj (truncation 2) (nerve D))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((homToNerveMk F ≫ CategoryTheory.Functor.map (truncation 2) (nerveMap G)).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f.edge :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ)
          (Functor.obj (truncation 2) (nerve D))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))

Tactic:
dsimp