-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst : W.IsMultiplicative
hW :
  ∀
    {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    (e : Edge x y), W (homMk e)
X Y : V.HomotopyCategory
fst fst_1 :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge fst fst_1
⊢ W (X :=
    mk
      (Sigma.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)
        (Sigma.mk (β :=
          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
          (Sigma.mk (β :=
            fun
              (y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            Edge fst y) fst_1 e))))
    (Y :=
    mk
      (Sigma.fst (β :=
        fun
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ↦
        Edge
          (Sigma.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)
            (Sigma.mk (β :=
              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
              (Sigma.mk (β :=
                fun
                  (y :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                Edge fst y) fst_1 e)))
          y)
        (Sigma.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)
          (Sigma.mk (β :=
            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
            (Sigma.mk (β :=
              fun
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              Edge fst y) fst_1 e)))))
    (homMk
      (Sigma.snd (β :=
        fun
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ↦
        Edge
          (Sigma.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)
            (Sigma.mk (β :=
              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
              (Sigma.mk (β :=
                fun
                  (y :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                Edge fst y) fst_1 e)))
          y)
        (Sigma.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)
          (Sigma.mk (β :=
            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
            (Sigma.mk (β :=
              fun
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              Edge fst y) fst_1 e)))))

Tactic:
exact hW e