-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ Eq (α :=
    ((Functor.obj Functor.curry (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
            (mk x₀)).obj
        (mk y) ⟶
      ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).obj (mk x₁)).obj (mk y))
    (NatTrans.app
      ((Functor.obj Functor.curry (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).map
          (homMk e) ≫
        Iso.hom
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              mkNatIso
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  Iso.refl
                    (((Functor.obj Functor.curry
                              (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                          (mk x)).obj
                      (mk y)))
                ⋯)
            x₁))
      (mk y))
    (NatTrans.app
      (Iso.hom
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              mkNatIso
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  Iso.refl
                    (((Functor.obj Functor.curry
                              (Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                          (mk x)).obj
                      (mk y)))
                ⋯)
            x₀) ≫
        (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e))
      (mk y))
have w : Eq (α :=
  Quiver.Hom (V := (tensorObj (𝒞 := Functor.category) X Y').HomotopyCategory)
    (mk
      (x₀,
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) :
            (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
              Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
          y))
    (mk
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1)) ◁
              g.app
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) :
          (a :
              X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) ⊗
                Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
            X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) ⊗
              Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
        (x₁, y))))
  (homMk
      (e.tensor
        (Edge.id
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (g.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) :
              (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            y))) ≫
    𝟙
      (mk
        (x₁,
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (g.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) :
              (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            y)))
  (𝟙
      (mk
        (x₀,
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (g.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) :
              (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) →
                Y'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            y)) ≫
    homMk
      (e.tensor
        (Edge.id
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (g.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      Edge._proof_1))) :
              (a : Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })) →
                Y'.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
            y))))
Tactic: simp