-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
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
⊢ 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)
have 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)))
Tactic: rw [MorphismProperty.ofHoms_iff]