-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
X Y : Cat
F : X ⟶ Y
x y : (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u)
f : x ⟶ y
⊢ Eq (α :=
    Quiver.Hom (V := (↑(ReflQuiv.forget.obj Y) : Type u))
      (Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        x)
      (Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        y))
    (Prefunctor.map
      (ReflPrefunctor.toPrefunctor
        ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
          Iso.hom
            ((fun (C : Cat.{u, u}) ↦
                (ofNerve₂ (↑C : Type u) :
                  ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅ ReflQuiv.of (↑C : Type u)))
              Y)))
      f)
    (Eq.recOn (motive :=
      fun (x_1 : (↑(ReflQuiv.forget.obj Y) : Type u))
        (x_2 :
          Prefunctor.obj
              (ReflPrefunctor.toPrefunctor
                (Iso.hom
                    ((fun (C : Cat.{u, u}) ↦
                        (ofNerve₂ (↑C : Type u) :
                          ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                            ReflQuiv.of (↑C : Type u)))
                      X) ≫
                  ReflQuiv.forget.map F))
              y =
            x_1) ↦
      Prefunctor.obj
          (ReflPrefunctor.toPrefunctor
            ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
              Iso.hom
                ((fun (C : Cat.{u, u}) ↦
                    (ofNerve₂ (↑C : Type u) :
                      ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                        ReflQuiv.of (↑C : Type u)))
                  Y)))
          x ⟶
        x_1)
      ⋯
      (Eq.recOn (motive :=
        fun (x_1 : (↑(ReflQuiv.forget.obj Y) : Type u))
          (x :
            Prefunctor.obj
                (ReflPrefunctor.toPrefunctor
                  (Iso.hom
                      ((fun (C : Cat.{u, u}) ↦
                          (ofNerve₂ (↑C : Type u) :
                            ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                              ReflQuiv.of (↑C : Type u)))
                        X) ≫
                    ReflQuiv.forget.map F))
                x =
              x_1) ↦
        x_1 ⟶
          Prefunctor.obj
            (ReflPrefunctor.toPrefunctor
              (Iso.hom
                  ((fun (C : Cat.{u, u}) ↦
                      (ofNerve₂ (↑C : Type u) :
                        ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                          ReflQuiv.of (↑C : Type u)))
                    X) ≫
                ReflQuiv.forget.map F))
            y)
        ⋯
        (Prefunctor.map
          (ReflPrefunctor.toPrefunctor
            (Iso.hom
                ((fun (C : Cat.{u, u}) ↦
                    (ofNerve₂ (↑C : Type u) :
                      ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                        ReflQuiv.of (↑C : Type u)))
                  X) ≫
              ReflQuiv.forget.map F))
          f)))
have obtain : ∀
  (f :
    (nerveFunctor₂.obj X).obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ Truncated.Edge._proof_2))),
  Eq (α :=
    Quiver.Hom (V := (↑(ReflQuiv.forget.obj Y) : Type u))
      (Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
            (a :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
          f))
      (Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((nerveFunctor₂.obj X).map (δ₂ 0 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
            (a :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
          f)))
    (Prefunctor.map
      (ReflPrefunctor.toPrefunctor
        ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
          Iso.hom
            ((fun (C : Cat.{u, u}) ↦
                (ofNerve₂ (↑C : Type u) :
                  ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅ ReflQuiv.of (↑C : Type u)))
              Y)))
      { edge := f, src_eq := sorry, tgt_eq := sorry })
    (Eq.recOn (motive :=
      fun (x : (↑(ReflQuiv.forget.obj Y) : Type u))
        (x_1 :
          Prefunctor.obj (V := (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u))
              (ReflPrefunctor.toPrefunctor
                (Iso.hom
                    ((fun (C : Cat.{u, u}) ↦
                        (ofNerve₂ (↑C : Type u) :
                          ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                            ReflQuiv.of (↑C : Type u)))
                      X) ≫
                  ReflQuiv.forget.map F))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((nerveFunctor₂.obj X).map (δ₂ 0 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
                f) =
            x) ↦
      Prefunctor.obj
          (ReflPrefunctor.toPrefunctor
            ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
              Iso.hom
                ((fun (C : Cat.{u, u}) ↦
                    (ofNerve₂ (↑C : Type u) :
                      ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                        ReflQuiv.of (↑C : Type u)))
                  Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
            f) ⟶
        x)
      sorry
      (Eq.recOn (motive :=
        fun (x : (↑(ReflQuiv.forget.obj Y) : Type u))
          (x_1 :
            Prefunctor.obj (V := (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u))
                (ReflPrefunctor.toPrefunctor
                  (Iso.hom
                      ((fun (C : Cat.{u, u}) ↦
                          (ofNerve₂ (↑C : Type u) :
                            ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                              ReflQuiv.of (↑C : Type u)))
                        X) ≫
                    ReflQuiv.forget.map F))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      ((nerveFunctor₂.obj X).map (δ₂ 1 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
                  f) =
              x) ↦
        x ⟶
          Prefunctor.obj (V := (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u))
            (ReflPrefunctor.toPrefunctor
              (Iso.hom
                  ((fun (C : Cat.{u, u}) ↦
                      (ofNerve₂ (↑C : Type u) :
                        ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                          ReflQuiv.of (↑C : Type u)))
                    X) ≫
                ReflQuiv.forget.map F))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((nerveFunctor₂.obj X).map (δ₂ 0 Truncated.Edge._proof_1 Truncated.Edge._proof_3).op) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj X).obj (op { obj := ⦋0 + 1⦌, property := Truncated.Edge._proof_3 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj X).obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
              f))
        sorry
        (Prefunctor.map
          (ReflPrefunctor.toPrefunctor
            (Iso.hom
                ((fun (C : Cat.{u, u}) ↦
                    (ofNerve₂ (↑C : Type u) :
                      ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                        ReflQuiv.of (↑C : Type u)))
                  X) ≫
              ReflQuiv.forget.map F))
          { edge := f, src_eq := sorry, tgt_eq := sorry })))
Tactic: obtain ⟨f, rfl, rfl⟩ := f
Cleared hypotheses: x, y, f