awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
⊢ homMk (Edge.id x) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (fst
                  (X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))
                  (Y.obj
                    (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 }))
            (x, y₁))) =
    𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (fst
                  (X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1)))
                  (Y.obj
                    (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 }))
            (x, y₀))) ≫
      𝟙 (mk x)
have rw : homMk (Edge.id x) =
  𝟙
      (mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (fst
                (X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1)))
                (Y.obj
                  (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 }))
          (x, y₀))) ≫
    𝟙 (mk x)
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y : Truncated 2
inst :
  Unique
    (X.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1)))
inst_1 :
  Subsingleton.{u + 1}
    (X.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ isoTerminal._proof_1)))
⊢ CategoryTheory.Prod.snd (↑Cat.chosenTerminal : Type u) Y.HomotopyCategory =
    (isoTerminal X).inv.toFunctor.prod (𝟭 Y.HomotopyCategory) ⋙ inverse X Y ⋙ mapHomotopyCategory (snd X Y)
have rw : Eq (α := (↑Cat.chosenTerminal : Type u) × Y.HomotopyCategory ⥤ Y.HomotopyCategory)
  (CategoryTheory.Prod.snd (↑Cat.chosenTerminal : Type u) Y.HomotopyCategory)
  ((isoTerminal X).inv.toFunctor.prod (𝟭 Y.HomotopyCategory) ⋙
    CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)
Tactic: rw [inverse_comp_mapHomotopyCategory_snd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y : Truncated 2
inst :
  Unique
    (Y.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1)))
inst_1 :
  Subsingleton.{u + 1}
    (Y.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ isoTerminal._proof_1)))
⊢ CategoryTheory.Prod.fst X.HomotopyCategory (↑Cat.chosenTerminal : Type u) =
    Functor.prod (𝟭 X.HomotopyCategory) (isoTerminal Y).inv.toFunctor ⋙ inverse X Y ⋙ mapHomotopyCategory (fst X Y)
have rw : Eq (α := X.HomotopyCategory × (↑Cat.chosenTerminal : Type u) ⥤ X.HomotopyCategory)
  (CategoryTheory.Prod.fst X.HomotopyCategory (↑Cat.chosenTerminal : Type u))
  (Functor.prod (𝟭 X.HomotopyCategory) (isoTerminal Y).inv.toFunctor ⋙
    CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)
Tactic: rw [inverse_comp_mapHomotopyCategory_fst]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
z :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) ≫
      𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₁)).obj
          (mk z)) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
have w : homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
  𝟙
      ((((Functor.obj Functor.curry₃
                    (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                      (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                        inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                          mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                (mk x)).obj
            (mk y₀)).obj
        (mk z)) ≫
    CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
      (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
Tactic: rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
z :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
w :
  homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) ≫
      𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₁)).obj
          (mk z)) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
have w₁ : homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
  CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
    (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
Tactic: rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
z :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
w :
  homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
w₁ :
  homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
      (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) ≫
      𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₁)).obj
          (mk z)) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
have w₂ : homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
  CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
    (Prod.mkHom (𝟙 (mk x)) (homMk (e.tensor (Edge.id z))))
Tactic: rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge y₀ y₁
z :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
w :
  homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
w₁ :
  homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
      (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
w₂ :
  homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
      (Prod.mkHom (𝟙 (mk x)) (homMk (e.tensor (Edge.id z))))
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) ≫
      𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₁)).obj
          (mk z)) =
    𝟙
        ((((Functor.obj Functor.curry₃
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                            mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      CategoryTheory.Functor.map (inverse X (tensorObj (𝒞 := Functor.category) Y Z))
        (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))
have w₃ : homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) = homMk ((Edge.id x).tensor (e.tensor (Edge.id z)))
Tactic: rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (associativity'Iso X Y Z).hom.app xyz =
    𝟙
      ((Equivalence.inverse (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
              inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙ mapHomotopyCategory (Iso.hom (α_ X Y Z))).obj
        xyz)
have change : 𝟙
      ((Equivalence.inverse (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
              inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙ mapHomotopyCategory (Iso.hom (α_ X Y Z))).obj
        xyz) ≫
    NatTrans.app
        (CategoryTheory.Functor.map (Equivalence.functor Functor.currying₃)
          (Iso.hom
            (mkNatIso
              (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))) ↦
                    mkNatIso
                      (fun
                          (z :
                            Z.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        Iso.refl
                          ((((Functor.obj Functor.curry₃
                                        (Equivalence.inverse
                                            (prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                              Z.HomotopyCategory) ⋙
                                          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                            inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙
                                              mapHomotopyCategory (Iso.hom (α_ X Y Z)))).obj
                                    (mk x)).obj
                                (mk y)).obj
                            (mk z)))
                      sorry)
                  sorry)
              sorry)))
        xyz ≫
      𝟙
        ((Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙ inverse X (tensorObj (𝒞 := Functor.category) Y Z)).obj
          xyz) =
  𝟙
    ((Equivalence.inverse (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
            inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙ mapHomotopyCategory (Iso.hom (α_ X Y Z))).obj
      xyz)
Tactic: change 𝟙 _ ≫ _ ≫ 𝟙 _ = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y : Truncated 2
x : X ⟶ Y
x_1 : Truncated 2
⊢ hoFunctor₂.map x ▷ hoFunctor₂.obj x_1 ≫ (iso Y x_1).symm.hom = (iso X x_1).symm.hom ≫ hoFunctor₂.map (x ▷ x_1)
have h : (hoFunctor₂.map x ▷ hoFunctor₂.obj x_1 ≫ (iso Y x_1).symm.hom).toFunctor =
  ((iso X x_1).symm.hom ≫ hoFunctor₂.map (x ▷ x_1)).toFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y x : Truncated 2
x_1 : X ⟶ Y
⊢ hoFunctor₂.obj x ◁ hoFunctor₂.map x_1 ≫ (iso x Y).symm.hom = (iso x X).symm.hom ≫ hoFunctor₂.map (x ◁ x_1)
have h : (hoFunctor₂.obj x ◁ hoFunctor₂.map x_1 ≫ (iso x Y).symm.hom).toFunctor =
  ((iso x X).symm.hom ≫ hoFunctor₂.map (x ◁ x_1)).toFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
x x_1 x_2 : Truncated 2
⊢ (iso x x_1).symm.hom ▷ hoFunctor₂.obj x_2 ≫
      Iso.hom (Iso.symm (iso (tensorObj (𝒞 := Functor.category) x x_1) x_2)) ≫ hoFunctor₂.map (Iso.hom (α_ x x_1 x_2)) =
    Iso.hom (α_ (hoFunctor₂.obj x) (hoFunctor₂.obj x_1) (hoFunctor₂.obj x_2)) ≫
      hoFunctor₂.obj x ◁ (iso x_1 x_2).symm.hom ≫ Iso.hom (Iso.symm (iso x (tensorObj (𝒞 := Functor.category) x_1 x_2)))
have h : ((iso x x_1).symm.hom ▷ hoFunctor₂.obj x_2 ≫
      Iso.hom (Iso.symm (iso (tensorObj (𝒞 := Functor.category) x x_1) x_2)) ≫
        hoFunctor₂.map (Iso.hom (α_ x x_1 x_2))).toFunctor =
  (Iso.hom (α_ (hoFunctor₂.obj x) (hoFunctor₂.obj x_1) (hoFunctor₂.obj x_2)) ≫
      hoFunctor₂.obj x ◁ (iso x_1 x_2).symm.hom ≫
        Iso.hom (Iso.symm (iso x (tensorObj (𝒞 := Functor.category) x_1 x_2)))).toFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
Y : Truncated 2
⊢ Iso.hom (λ_ (hoFunctor₂.obj Y)) =
    Iso.hom (Iso.symm (HomotopyCategory.isoTerminal ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)))) ▷ hoFunctor₂.obj Y ≫
      Iso.hom (Iso.symm (iso ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)) Y)) ≫ hoFunctor₂.map (Iso.hom (λ_ Y))
have h : Cat.Hom.toFunctor (Iso.hom (λ_ (hoFunctor₂.obj Y))) =
  (Iso.hom (Iso.symm (HomotopyCategory.isoTerminal ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)))) ▷ hoFunctor₂.obj Y ≫
      Iso.hom (Iso.symm (iso ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)) Y)) ≫
        hoFunctor₂.map (Iso.hom (λ_ Y))).toFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X : Truncated 2
⊢ Iso.hom (ρ_ (hoFunctor₂.obj X)) =
    hoFunctor₂.obj X ◁ Iso.hom (Iso.symm (HomotopyCategory.isoTerminal ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)))) ≫
      Iso.hom (Iso.symm (iso X ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)))) ≫ hoFunctor₂.map (Iso.hom (ρ_ X))
have h : Cat.Hom.toFunctor (Iso.hom (ρ_ (hoFunctor₂.obj X))) =
  (hoFunctor₂.obj X ◁ Iso.hom (Iso.symm (HomotopyCategory.isoTerminal ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)))) ≫
      Iso.hom (Iso.symm (iso X ((𝟙_ (Truncated 2)) (𝒞 := Functor.category)))) ≫
        hoFunctor₂.map (Iso.hom (ρ_ X))).toFunctor
Tactic: ext