awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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 (β :=
          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 ⋯
have 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 sorry) =
  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 sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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₂
⊢ 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₂)))
have 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)
Tactic: dsimp [forget]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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₂
⊢ 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)
have 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)
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      K₁.X ◁ g.f)
have erw : Eq (α :=
  (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ L₂).X)
  (Hom.f (K₁ ◁ g)) (K₁.X ◁ g.f)
Tactic: erw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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
⊢ 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₂)))
have 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)
Tactic: dsimp [forget]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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
⊢ 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)
have 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)
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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₂))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      f.f ▷ K₂.X)
have erw : Eq (α :=
  (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ K₂).X)
  (Hom.f (f ▷ K₂)) (f.f ▷ K₂.X)
Tactic: erw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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₂
⊢ 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₂)))
have 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)
Tactic: dsimp [forget]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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₂
⊢ 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)
have 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))
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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))
    (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I) K₁.X K₂.X) ≫
      (f.f ⊗ₘ g.f))
have erw : Eq (α :=
  (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K₁ K₂).X ⟶
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) L₁ L₂).X)
  (Hom.f (f ⊗ₘ g)) (f.f ⊗ₘ g.f)
Tactic: erw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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
⊢ 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)
have 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)
Tactic: simp only [tensorHom_id, whiskerRight_tensor, id_whiskerRight,
      id_comp, Iso.inv_hom_id, comp_id, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Monoidal (goal)
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
⊢ 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)
have 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)
Tactic: erw [id_whiskerRight]