-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
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₁
refine_1 :
  ComposableArrows.left (n := 1)
      (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.left (n := 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)
refine_2 :
  ComposableArrows.right (n := 1)
      (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.right (n := 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)
⊢ 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⦌ ⋯)))
    (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⦌ ⋯))) :
          (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⦌ ⋯)))

Tactic:
refine ComposableArrows.ext₁ ?_ ?_ rfl

Premises used: CategoryTheory.ComposableArrows.ext₁