awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ L₁ K₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
erw :
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ L₂).X)
    (Hom.f (f ⊗ₘ g)) (f.f ⊗ₘ g.f)
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ L₂).X)
    (Hom.f (f ⊗ₘ g))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      (f.f ⊗ₘ g.f))

Tactic:
erw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ L₁ K₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ L₂).X)
    (Hom.f (f ⊗ₘ g)) (f.f ⊗ₘ g.f)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
simp :
  Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ▷
          K₃.X ≫
        Iso.hom (α_ K₁.X K₂.X K₃.X)
⊢ Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
        (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ⊗ₘ
          𝟙 K₃.X)) ≫
      Iso.hom (α_ K₁.X K₂.X K₃.X) ≫
        (𝟙 K₁.X ⊗ₘ
            𝟙
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₂.X
                K₃.X)) ≫
          𝟙
            (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X
              (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₂ K₃).X)

Tactic:
simp only [tensorHom_id, whiskerRight_tensor, id_whiskerRight,
      id_comp, Iso.inv_hom_id, comp_id, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.whiskerRight_tensor, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
erw :
  Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
        Iso.hom (α_ K₁.X K₂.X K₃.X)
⊢ Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ▷
          K₃.X ≫
        Iso.hom (α_ K₁.X K₂.X K₃.X)

Tactic:
erw [id_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
rw :
  Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      Iso.hom (α_ K₁.X K₂.X K₃.X)
⊢ Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
        Iso.hom (α_ K₁.X K₂.X K₃.X)

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
erw :
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂)
          K₃).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₂ K₃)).X)
    (Hom.f (Iso.hom (α_ K₁ K₂ K₃))) (Iso.hom (α_ K₁.X K₂.X K₃.X))
⊢ Hom.f (Iso.hom (α_ K₁ K₂ K₃)) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X K₃.X) ≫
      Iso.hom (α_ K₁.X K₂.X K₃.X)

Tactic:
erw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂)
          K₃).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁
          (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₂ K₃)).X)
    (Hom.f (Iso.hom (α_ K₁ K₂ K₃))) (Iso.hom (α_ K₁.X K₂.X K₃.X))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
dsimp :
  CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
              ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))
            (Functor.obj (forget C c) K)) ≫
        (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K))) ≫
      Iso.hom (λ_ (Functor.obj (forget C c) K))
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
                  ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))
                (Functor.obj (forget C c) K))) ≪≫
          (Iso.symm (tensorUnitIso C c) ⊗ᵢ Iso.refl (Functor.obj (forget C c) K))) ≪≫
        λ_ (Functor.obj (forget C c) K)).hom

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
erw :
  Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)) K) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)))
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
        ((𝟙_ (GradedObject I C)) (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I))
        (Functor.obj (forget C c) K))
      (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K)) (Iso.hom (λ_ (Functor.obj (forget C c) K))))
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
              ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))
            (Functor.obj (forget C c) K)) ≫
        (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K))) ≫
      Iso.hom (λ_ (Functor.obj (forget C c) K))

Tactic:
erw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)) K) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (λ_ K)))
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
        ((𝟙_ (GradedObject I C)) (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I))
        (Functor.obj (forget C c) K))
      (Iso.inv (tensorUnitIso C c) ⊗ₘ 𝟙 (Functor.obj (forget C c) K)) (Iso.hom (λ_ (Functor.obj (forget C c) K))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
dsimp :
  CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (forget C c) K)
            (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
              ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
        (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c))) ≫
      Iso.hom (ρ_ (Functor.obj (forget C c) K))
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
                (Functor.obj (forget C c) K)
                (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
                  ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))))) ≪≫
          (Iso.refl (Functor.obj (forget C c) K) ⊗ᵢ Iso.symm (tensorUnitIso C c))) ≪≫
        ρ_ (Functor.obj (forget C c) K)).hom

Tactic:
dsimp