-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x y
rw :
  ∃ (i :
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) ×
      (y :
        V.obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
              OneTruncation₂._proof_1))) ×
        Edge x y),
    Arrow.mk (homMk e) =
      Arrow.mk
        (homMk
          (i.snd (β :=
                fun
                  (x :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ×
                  Edge x y).snd
            (β :=
            fun
              (y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            Edge
              (i.fst (β :=
                fun
                  (x :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ×
                  Edge x y))
              y)))
⊢ MorphismProperty.ofHoms (X :=
    fun
      (e :
        (x :
          V.obj
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                OneTruncation₂._proof_1))) ×
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ×
            Edge x y) ↦
    mk
      (e.fst (β :=
        fun
          (x :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ↦
        (y :
          V.obj
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                OneTruncation₂._proof_1))) ×
          Edge x y)))
    (Y :=
    fun
      (e :
        (x :
          V.obj
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                OneTruncation₂._proof_1))) ×
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ×
            Edge x y) ↦
    mk
      (e.snd (β :=
            fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y).fst
        (β :=
        fun
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ↦
        Edge
          (e.fst (β :=
            fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y))
          y)))
    (fun
        (e :
          (x :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ×
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y) ↦
      homMk
        (e.snd (β :=
              fun
                (x :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ×
                Edge x y).snd
          (β :=
          fun
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          Edge
            (e.fst (β :=
              fun
                (x :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ×
                Edge x y))
            y)))
    (homMk e)

Tactic:
rw [MorphismProperty.ofHoms_iff]

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff