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
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
i j : I
hij : c.Rel i j
pos :
  Iso.inv (ρ_ (K.X i)) ≫
      K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        HSMul.hSMul (α := ℤˣ) (β :=
          MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0) ⟶
            X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
          1
          (K.d i j ▷ X.{v_1, u_1, u_2} (tensorUnit C c) 0 ≫
            K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫
      Iso.inv (ρ_ (K.X j)) ≫
        K.X j ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          K.ιTensorObj (tensorUnit C c) j 0 j ⋯
⊢ Iso.inv (ρ_ (K.X i)) ≫
      K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        HSMul.hSMul (β :=
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (K.X i))
              (X.{v_1, u_1, u_2} (tensorUnit C c) 0) ⟶
            X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
          (c.ε₁ c c (i, 0))
          (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (K.d i j))
              (X.{v_1, u_1, u_2} (tensorUnit C c) 0) ≫
            K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫
      Iso.inv (ρ_ (K.X j)) ≫
        K.X j ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          K.ιTensorObj (tensorUnit C c) j 0 j ⋯

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
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
i j : I
hij : c.Rel i j
⊢ Iso.inv (ρ_ (K.X i)) ≫
      K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        HSMul.hSMul (α := ℤˣ) (β :=
          MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0) ⟶
            X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
          1
          (K.d i j ▷ X.{v_1, u_1, u_2} (tensorUnit C c) 0 ≫
            K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫
      Iso.inv (ρ_ (K.X j)) ≫
        K.X j ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          K.ιTensorObj (tensorUnit C c) j 0 j ⋯

Tactic:
simp only [one_smul, whisker_exchange_assoc, whiskerRight_id, assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, one_smul, CategoryTheory.MonoidalCategory.whiskerRight_id
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
i j : I
hij : ¬c.Rel i j
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (K.tensorObj (tensorUnit C c)).X j)
    (Iso.inv K.rightUnitor' i ≫ (K.tensorObj (tensorUnit C c)).d i j : K.X i ⟶ (K.tensorObj (tensorUnit C c)).X j)
    (K.d i j ≫ Iso.inv K.rightUnitor' j : K.X i ⟶ (K.tensorObj (tensorUnit C c)).X j)

Tactic:
simp only [shape _ _ _ hij, comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- 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₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
g : K₂ ⟶ L₂
dsimp :
  Hom.f (K₁ ◁ g) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      K₁.X ◁ g.f ≫
        𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X L₂.X)
⊢ CategoryTheory.Functor.map (forget C c) (K₁ ◁ g) =
    Iso.inv
        (Iso.refl
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (forget C c) K₁) (Functor.obj (forget C c) K₂))) ≫
      Functor.obj (forget C c) K₁ ◁ CategoryTheory.Functor.map (forget C c) g ≫
        Iso.hom
          (Iso.refl
            (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
              (Functor.obj (forget C c) K₁) (Functor.obj (forget C c) L₂)))

Tactic:
dsimp [forget]

Premises used: HomologicalComplex.forget
-- 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₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
g : K₂ ⟶ L₂
rw :
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ L₂).X)
    (Hom.f (K₁ ◁ g))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      K₁.X ◁ g.f)
⊢ Hom.f (K₁ ◁ g) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      K₁.X ◁ g.f ≫
        𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X L₂.X)

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
g : K₂ ⟶ L₂
erw :
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ L₂).X)
    (Hom.f (K₁ ◁ g)) (K₁.X ◁ g.f)
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ L₂).X)
    (Hom.f (K₁ ◁ g))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      K₁.X ◁ 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₁ K₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
g : K₂ ⟶ L₂
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ L₂).X)
    (Hom.f (K₁ ◁ g)) (K₁.X ◁ 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₁ L₁ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex.{v_1, u_1, u_2} C c
dsimp :
  Hom.f (f ▷ K₂) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      f.f ▷ K₂.X ≫
        𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) L₁.X K₂.X)
⊢ CategoryTheory.Functor.map (forget C c) (f ▷ K₂) =
    Iso.inv
        (Iso.refl
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (forget C c) K₁) (Functor.obj (forget C c) K₂))) ≫
      CategoryTheory.Functor.map (forget C c) f ▷ Functor.obj (forget C c) K₂ ≫
        Iso.hom
          (Iso.refl
            (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
              (Functor.obj (forget C c) L₁) (Functor.obj (forget C c) K₂)))

Tactic:
dsimp [forget]

Premises used: HomologicalComplex.forget
-- 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₁ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex.{v_1, u_1, u_2} C c
rw :
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ K₂).X)
    (Hom.f (f ▷ K₂))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      f.f ▷ K₂.X)
⊢ Hom.f (f ▷ K₂) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      f.f ▷ K₂.X ≫
        𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) L₁.X K₂.X)

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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₁ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex.{v_1, u_1, u_2} C c
erw :
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ K₂).X)
    (Hom.f (f ▷ K₂)) (f.f ▷ K₂.X)
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ K₂).X)
    (Hom.f (f ▷ K₂))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      f.f ▷ 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₁ L₁ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ K₂).X)
    (Hom.f (f ▷ K₂)) (f.f ▷ 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₁ L₁ K₂ L₂ : HomologicalComplex.{v_1, u_1, u_2} C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
dsimp :
  Hom.f (f ⊗ₘ g) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      (f.f ⊗ₘ g.f) ≫
        𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) L₁.X L₂.X)
⊢ CategoryTheory.Functor.map (forget C c) (f ⊗ₘ g) =
    Iso.inv
        (Iso.refl
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (forget C c) K₁) (Functor.obj (forget C c) K₂))) ≫
      (CategoryTheory.Functor.map (forget C c) f ⊗ₘ CategoryTheory.Functor.map (forget C c) g) ≫
        Iso.hom
          (Iso.refl
            (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
              (Functor.obj (forget C c) L₁) (Functor.obj (forget C c) L₂)))

Tactic:
dsimp [forget]

Premises used: HomologicalComplex.forget
-- 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₂
rw :
  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))
⊢ Hom.f (f ⊗ₘ g) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      (f.f ⊗ₘ g.f) ≫
        𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) L₁.X L₂.X)

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id