awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
ex : Edge x₀ x₁
ey : Edge y₀ y₁
dsimp : (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
⊢ Eq (α :=
    (functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)) ⟶
      Functor.obj (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (mk (x₁, y₁)))
    ((functor X Y ⋙ inverse X Y).map (homMk (ex.tensor ey)) ≫
      Iso.hom
        ((fun
              (x :
                (tensorObj (𝒞 := Functor.category) X Y).obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
              (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
          (x₁, y₁)))
    (Iso.hom
        ((fun
              (x :
                (tensorObj (𝒞 := Functor.category) X Y).obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
              (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
          (x₀, y₀)) ≫
      CategoryTheory.Functor.map (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (homMk (ex.tensor ey)))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
ex : Edge x₀ x₁
ey : Edge y₀ y₁
rw : (inverse X Y).map (homMk ex, homMk ey) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
rw₁ : (inverse X Y).map (homMk ex, homMk ey) = homMk (ex.tensor ey)
rw₂ rw₃ : homMk (ex.tensor ey) = homMk (ex.tensor ey)
⊢ (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)

Tactic:
rw [Category.comp_id, Category.id_comp, inverse_map_mkHom_homMk_homMk]

Premises used: CategoryTheory.Category.comp_id, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ (functorCompInverseIso X Y).hom.app (mk (x, y)) = 𝟙 ((functor X Y ⋙ inverse X Y).obj (mk (x, y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ Eq (α :=
    Functor.obj (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (mk (x, y)) ⟶
      (functor X Y ⋙ inverse X Y).obj (mk (x, y)))
    ((functorCompInverseIso X Y).inv.app (mk (x, y)))
    (𝟙 (Functor.obj (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (mk (x, y))))

Tactic:
rfl

Premises used: SSet.Truncated.HomotopyCategory.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ (inverseCompFunctorIso X Y).hom.app (mk x, mk y) = 𝟙 ((inverse X Y ⋙ functor X Y).obj (mk x, mk y))

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, CategoryTheory.Quotient.comp, Quiver.Path.comp, SSet.Truncated.HomotopyCategory.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ (inverseCompFunctorIso X Y).inv.app (mk x, mk y) =
    𝟙 (Functor.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory)) (mk x, mk y))

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, CategoryTheory.Quotient.comp, Quiver.Path.comp, SSet.Truncated.HomotopyCategory.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
⊢ functor X Y ⋙ inverse X Y = 𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory

Tactic:
Functor.ext_of_iso (functorCompInverseIso X Y) (fun _ ↦ rfl)

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
⊢ inverse X Y ⋙ functor X Y = 𝟭 (X.HomotopyCategory × Y.HomotopyCategory)

Tactic:
Functor.ext_of_iso (inverseCompFunctorIso X Y) (fun _ ↦ rfl)

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
h :
  Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (X.HomotopyCategory × Y.HomotopyCategory)) { toFunctor := functor X Y }
        { toFunctor := inverse X Y }) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
⊢ CategoryStruct.comp (Y := Cat.of (X.HomotopyCategory × Y.HomotopyCategory)) { toFunctor := functor X Y }
      { toFunctor := inverse X Y } =
    𝟙 (Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
⊢ Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (X.HomotopyCategory × Y.HomotopyCategory)) { toFunctor := functor X Y }
        { toFunctor := inverse X Y }) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))

Tactic:
functor_comp_inverse X Y

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, SSet.Truncated.HomotopyCategory
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
⊢ Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (X.HomotopyCategory × Y.HomotopyCategory)) { toFunctor := functor X Y }
        { toFunctor := inverse X Y }) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))

Tactic:
exact functor_comp_inverse X Y

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
h :
  Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
        { toFunctor := inverse X Y } { toFunctor := functor X Y }) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory)))
⊢ CategoryStruct.comp (Y := Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
      { toFunctor := inverse X Y } { toFunctor := functor X Y } =
    𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
⊢ Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
        { toFunctor := inverse X Y } { toFunctor := functor X Y }) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory)))

Tactic:
inverse_comp_functor X Y

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
⊢ Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
        { toFunctor := inverse X Y } { toFunctor := functor X Y }) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory)))

Tactic:
exact inverse_comp_functor X Y

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
f : X ⟶ X'
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))
⊢ homMk ((e.map f).tensor (Edge.id y)) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (f.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 })) →
                  X'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              x₁,
            y)) =
    𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (f.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 })) →
                  X'.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              x₀,
            y)) ≫
      homMk ((e.map f).tensor (Edge.id y))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y : Truncated 2
f : X ⟶ X'
⊢ (mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y = inverse X Y ⋙ mapHomotopyCategory (f ▷ Y)

Tactic:
Functor.ext_of_iso (mapHomotopyCategoryProdIdCompInverseIso _ _) (fun _ ↦ rfl)

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategoryProdIdCompInverseIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Y' : Truncated 2
g : Y ⟶ Y'
⊢ Functor.prod (𝟭 X.HomotopyCategory) (mapHomotopyCategory g) ⋙ inverse X Y' = inverse X Y ⋙ mapHomotopyCategory (X ◁ g)

Tactic:
Functor.ext_of_iso (idProdMapHomotopyCategoryCompInverseIso _ _) (fun _ ↦ rfl)

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.idProdMapHomotopyCategoryCompInverseIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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₁
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)
⊢ 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)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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 x)

Tactic:
homMk_id x

Premises used: SSet.Truncated.HomotopyCategory.homMk_id, CategoryTheory.Quotient.comp, Quiver.Path.comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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 x)

Tactic:
exact homMk_id x

Premises used: SSet.Truncated.HomotopyCategory.homMk_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
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 (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₀)).obj (mk y) ⟶
      Functor.obj
        (Functor.obj (Functor.obj Functor.curry (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory))
          (mk x₁))
        (mk y))
    (NatTrans.app
      ((Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst 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 (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj
                        (mk y)))
                  ⋯ :
                (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x) ≅
                  Functor.obj
                    (Functor.obj Functor.curry (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)) (mk x)))
            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 (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj
                        (mk y)))
                  ⋯ :
                (Functor.obj Functor.curry (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x) ≅
                  Functor.obj
                    (Functor.obj Functor.curry (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)) (mk x)))
            x₀) ≫
        CategoryTheory.Functor.map
          (Functor.obj Functor.curry (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)) (homMk e))
      (mk y))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
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))
⊢ homMk (Edge.id y) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (snd
                  (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 })) →
                Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
            (x₁, y))) =
    𝟙
      (mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (snd
                (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 })) →
              Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
          (x₀, y)))

Tactic:
homMk_id y

Premises used: SSet.Truncated.HomotopyCategory.homMk_id, CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, SSet.Truncated.HomotopyCategory.homMk, Quiver.Path.comp