-- 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₁
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)
⊢ 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⦌ ⋯)))
have 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⦌ sorry))) :
        (a : X.obj (op { obj := ⦋1⦌, property := sorry })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := sorry }))
      f.edge)
Tactic: refine ComposableArrows.ext₁ ?_ ?_ rfl