-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X Y : Cat
F : X ⟶ Y
x y : (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u)
f : x ⟶ y
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 := ⋯, tgt_eq := ⋯ })
      (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)
        ⋯
        (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))
          ⋯
          (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 := ⋯, tgt_eq := ⋯ })))
⊢ 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)))

Tactic:
obtain ⟨f, rfl, rfl⟩ := f

Premises used: rfl