awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact homMk_id y

Premises used: SSet.Truncated.HomotopyCategory.homMk_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
⊢ inverse X Y ⋙ mapHomotopyCategory (fst X Y) = CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory

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

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategoryFstIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
⊢ inverse X Y ⋙ mapHomotopyCategory (snd X Y) = CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory

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

Premises used: CategoryTheory.Functor.ext_of_iso, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategorySndIso, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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)))
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)
⊢ CategoryTheory.Prod.snd (↑Cat.chosenTerminal : Type u) Y.HomotopyCategory =
    (isoTerminal X).inv.toFunctor.prod (𝟭 Y.HomotopyCategory) ⋙ inverse X Y ⋙ mapHomotopyCategory (snd X Y)

Tactic:
rw [inverse_comp_mapHomotopyCategory_snd]

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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)))
⊢ 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:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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)))
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)
⊢ CategoryTheory.Prod.fst X.HomotopyCategory (↑Cat.chosenTerminal : Type u) =
    Functor.prod (𝟭 X.HomotopyCategory) (isoTerminal Y).inv.toFunctor ⋙ inverse X Y ⋙ mapHomotopyCategory (fst X Y)

Tactic:
rw [inverse_comp_mapHomotopyCategory_fst]

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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)))
⊢ 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:
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.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
z₀ z₁ :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge z₀ z₁
⊢ CategoryTheory.Functor.map (mapHomotopyCategory (Iso.hom (α_ X Y Z)))
      (CategoryTheory.Functor.map (inverse (tensorObj (𝒞 := Functor.category) X Y) Z)
        (Prod.mkHom (𝟙 ((inverse X Y).obj (mk x, mk y))) (homMk e))) =
    homMk ((Edge.id x).tensor ((Edge.id y).tensor e))

Tactic:
dsimp [← Edge.id_tensor_id]

Premises used: SSet.Truncated.Edge.id_tensor_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₁
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))))
w₃ w₄ : homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) = homMk ((Edge.id x).tensor (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))))

Tactic:
rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, CategoryTheory.Category.comp_id, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, CategoryTheory.Category.id_comp
-- 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))
z :
  Z.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ Eq (α :=
    (((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₃
                    (Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙
                      inverse X (tensorObj (𝒞 := Functor.category) Y Z))).obj
                (mk x₁)).obj
            (mk y)).obj
        (mk z))
    (homMk (e.tensor (Y := tensorObj (𝒞 := Functor.category) Y Z) (y := (y, z)) (Edge.id (y, 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 (homMk e) ((inverse Y Z).map (𝟙 (mk y), 𝟙 (mk z)))))

Tactic:
simp only [Category.comp_id, Category.id_comp, ← prod_id',
          CategoryTheory.Functor.map_id, inverse_obj, inverse_map_mkHom_homMk_id]

Premises used: CategoryTheory.prod_id', CategoryTheory.Category.comp_id, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, CategoryTheory.Functor.map_id, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Z : Truncated 2
⊢ (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
      inverse (tensorObj (𝒞 := Functor.category) X Y) Z ⋙ mapHomotopyCategory (Iso.hom (α_ X Y Z)) =
    Equivalence.functor (prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory) ⋙
      Functor.prod (𝟭 X.HomotopyCategory) (inverse Y Z) ⋙ inverse X (tensorObj (𝒞 := Functor.category) Y Z)

Tactic:
Functor.ext_of_iso (associativityIso _ _ _) (fun _ ↦ rfl) associativityIso_hom_app

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso, CategoryTheory.Functor.ext_of_iso, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x : X ⟶ Y
x_1 : Truncated 2
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
⊢ hoFunctor₂.map x ▷ hoFunctor₂.obj x_1 ≫ (iso Y x_1).symm.hom = (iso X x_1).symm.hom ≫ hoFunctor₂.map (x ▷ x_1)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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).toFunctor =
    ((iso X x_1).symm.hom ≫ hoFunctor₂.map (x ▷ x_1)).toFunctor

Tactic:
apply mapHomotopyCategory_prod_id_comp_inverse

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y x : Truncated 2
x_1 : X ⟶ Y
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
⊢ hoFunctor₂.obj x ◁ hoFunctor₂.map x_1 ≫ (iso x Y).symm.hom = (iso x X).symm.hom ≫ hoFunctor₂.map (x ◁ x_1)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y x : Truncated 2
x_1 : X ⟶ Y
⊢ (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:
apply id_prod_mapHomotopyCategory_comp_inverse

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
x x_1 x_2 : Truncated 2
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
⊢ (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)))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
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))).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:
apply associativity

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.associativity
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
Y : Truncated 2
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
⊢ 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))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
Y : Truncated 2
⊢ 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:
apply left_unitality

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X : Truncated 2
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
⊢ 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))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X : Truncated 2
⊢ 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:
apply right_unitality

Premises used: SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X : SSet
x : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ X
⊢ Eq (α := (↑Cat.chosenTerminal : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))
    ((unitHomEquiv X : (a : 𝟙_ SSet ⟶ X) → (↑Cat.chosenTerminal : Type u) ⥤ (↑(hoFunctor.obj X) : Type u)) x :
      (↑Cat.chosenTerminal : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))
    (Cat.Hom.toFunctor (Functor.LaxMonoidal.ε hoFunctor) ⋙ (hoFunctor.map x).toFunctor :
      (↑((𝟙_ Cat) (𝒞 := Cat.category)) : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, CategoryTheory.Functor.comp, CategoryTheory.Cat.of, CategoryTheory.Bundled.of, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
⊢ Functor.Additive (D := SSet ⥤ ChainComplex.{v, u, 0} C ℕ)
    (Functor.obj (Functor.obj Functor.postcompose₂ (AlgebraicTopology.alternatingFaceMapComplex C))
      (sigmaConst ⋙ Functor.whiskeringRight SimplexCategoryᵒᵖ (Type w) C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} SSet C
dsimp :
  Eq.{v + 1} (α := F.obj Δ[n] ⟶ F.obj Δ[n])
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : Δ[n] _⦋n⦌) ↦ F.obj Δ[n])
        (Sigma.ι.{w, v, u} (β := Δ[n] _⦋n⦌) (C := C) (fun (x : Δ[n] _⦋n⦌) ↦ F.obj Δ[n])
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌))
        (Sigma.desc fun (α : Δ[n] _⦋n⦌) ↦ F.map ((Equiv.symm yonedaEquiv : (a : Δ[n] _⦋n⦌) → Δ[n] ⟶ Δ[n]) α)) :
      F.obj Δ[n] ⟶ F.obj Δ[n])
    (𝟙 (F.obj Δ[n]) : F.obj Δ[n] ⟶ F.obj Δ[n])
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F ⟶ Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := CategoryTheory.Functor.{w, v, w + 1, u} SSet C) (Functor.obj (evaluation SSet C) Δ[n])
          (Functor.obj
            (Functor.obj (C := C ⥤ SSet ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (Functor.obj Functor.postcompose₂ (HomologicalComplex.eval C (ComplexShape.down ℕ) n))
              (chainComplexFunctor C))
            (Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)))
        (NatTrans.app
          {
            app := fun (R : C) ↦
              Sigma.ι.{w, v, u} (β := Δ[n] _⦋n⦌) (C := C) (fun (x : Δ[n] _⦋n⦌) ↦ R)
                ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) :
                  Δ[n] _⦋n⦌),
            naturality := ⋯ }
          (Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F))
        (CategoryTheory.Functor.map (Functor.obj (evaluation SSet C) Δ[n])
          (NatTrans.app
            {
              app := fun (F : CategoryTheory.Functor.{w, v, w + 1, u} SSet C) ↦
                {
                  app := fun (S : SSet.{w}) ↦
                    Sigma.desc fun (α : S _⦋n⦌) ↦ F.map ((Equiv.symm yonedaEquiv : (a : S _⦋n⦌) → Δ[n] ⟶ S) α),
                  naturality := ⋯ },
              naturality := ⋯ }
            F)) :
      Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F ⟶ Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)
    (𝟙 (Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F) :
      Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F ⟶ Functor.obj (Functor.obj (evaluation SSet C) Δ[n]) F)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} SSet C
⊢ Eq.{v + 1} (α := F.obj Δ[n] ⟶ F.obj Δ[n])
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : Δ[n] _⦋n⦌) ↦ F.obj Δ[n])
        (Sigma.ι.{w, v, u} (β := Δ[n] _⦋n⦌) (C := C) (fun (x : Δ[n] _⦋n⦌) ↦ F.obj Δ[n])
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌))
        (Sigma.desc fun (α : Δ[n] _⦋n⦌) ↦ F.map ((Equiv.symm yonedaEquiv : (a : Δ[n] _⦋n⦌) → Δ[n] ⟶ Δ[n]) α)) :
      F.obj Δ[n] ⟶ F.obj Δ[n])
    (𝟙 (F.obj Δ[n]) : F.obj Δ[n] ⟶ F.obj Δ[n])

Tactic:
simp