-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : X ⟶ Functor.obj (truncation 2) (nerve C)
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
⊢ Eq (α :=
    Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((homToNerveMk (descOfTruncation φ)).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⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.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⦌ ⋯)))
have simp : Eq (α :=
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry)))
  (ComposableArrows.mk₁ (X₀ :=
      (nerveEquiv : (a : ComposableArrows C 0) → C)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
              (a : X.obj (op { obj := ⦋0⦌, property := _proof_1 })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
            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⦌ _proof_1))))
      (X₁ :=
      (nerveEquiv : (a : ComposableArrows C 0) → C)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
              (a : X.obj (op { obj := ⦋0⦌, property := _proof_1 })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
            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⦌ _proof_1))))
      ((nerve.homEquiv :
          (a :
              SSet.Edge
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := Edge._proof_1 })) :
                    (a : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })) →
                      ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
                  x₀)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := Edge._proof_1 })) :
                    (a : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })) →
                      ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
                  x₁)) →
            (nerveEquiv : (a : ComposableArrows C 0) → C)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := Edge._proof_1 })) :
                    (a : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })) →
                      ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
                  x₀) ⟶
              (nerveEquiv : (a : ComposableArrows C 0) → C)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := Edge._proof_1 })) :
                    (a : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })) →
                      ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
                  x₁))
        (f.map φ)) :
    ComposableArrows C 1)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry))) :
        (a : X.obj (op { obj := ⦋1⦌, property := sorry })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := sorry }))
      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⦌ sorry)))
Tactic: simp only [homToNerveMk_app_edge, descOfTruncation_obj_mk,
        descOfTruncation_map_homMk]