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 : I
dsimp :
  Eq.{v_1 + 1} (α := K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
        GradedObject.Monoidal.tensorObj.{u_2, v_1, u_1} K.X
          (Functor.obj (GradedObject.single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) i)
        (Iso.inv (GradedObject.Monoidal.rightUnitor K.X) i)
        (GradedObject.Monoidal.tensorHom (𝟙 K.X) (Iso.hom (tensorUnitIso C c)) i) :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
    (Iso.inv (ρ_ (K.X i)) ≫
        K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          K.ιTensorObj (tensorUnit C c) i 0 i ⋯ :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
    (Iso.inv K.rightUnitor' i : K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
    (Iso.inv (ρ_ (K.X i)) ≫
        K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          K.ιTensorObj (tensorUnit C c) i 0 i ⋯ :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)

Tactic:
dsimp [rightUnitor']

Premises used: HomologicalComplex.rightUnitor'
-- 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 : I
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0))
      (K.X i ◁ Iso.inv GradedObject.Monoidal.tensorUnit₀)
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
        (𝟙 K.X i ⊗ₘ Iso.hom (tensorUnitIso C c) 0)
        (GradedObject.Monoidal.ιTensorObj K.X (X.{v_1, u_1, u_2} (tensorUnit C c)) i 0 i ⋯)))
    (K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      K.ιTensorObj (tensorUnit C c) i 0 i ⋯)
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
        GradedObject.Monoidal.tensorObj.{u_2, v_1, u_1} K.X
          (Functor.obj (GradedObject.single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) i)
        (Iso.inv (GradedObject.Monoidal.rightUnitor K.X) i)
        (GradedObject.Monoidal.tensorHom (𝟙 K.X) (Iso.hom (tensorUnitIso C c)) i) :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)
    (Iso.inv (ρ_ (K.X i)) ≫
        K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          K.ιTensorObj (tensorUnit C c) i 0 i ⋯ :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X i)

Tactic:
rw [GradedObject.Monoidal.rightUnitor_inv_apply, assoc, assoc, Iso.cancel_iso_inv_left,
    GradedObject.Monoidal.ι_tensorHom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GradedObject.Monoidal.rightUnitor_inv_apply, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.GradedObject.Monoidal.ι_tensorHom
-- 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 : I
dsimp :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0))
      (K.X i ◁ Iso.inv GradedObject.Monoidal.tensorUnit₀)
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
        (𝟙 (K.X i) ⊗ₘ Iso.hom (tensorUnitIso C c) 0)
        (GradedObject.Monoidal.ιTensorObj K.X (X.{v_1, u_1, u_2} (tensorUnit C c)) i 0 i ⋯)))
    (K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      K.ιTensorObj (tensorUnit C c) i 0 i ⋯)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0))
      (K.X i ◁ Iso.inv GradedObject.Monoidal.tensorUnit₀)
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
        (𝟙 K.X i ⊗ₘ Iso.hom (tensorUnitIso C c) 0)
        (GradedObject.Monoidal.ιTensorObj K.X (X.{v_1, u_1, u_2} (tensorUnit C c)) i 0 i ⋯)))
    (K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      K.ιTensorObj (tensorUnit C c) i 0 i ⋯)

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 : I
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
      (K.X i ◁
        CategoryStruct.comp (Y := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0)
          (Iso.inv GradedObject.Monoidal.tensorUnit₀) (Iso.hom (tensorUnitIso C c) 0))
      (GradedObject.Monoidal.ιTensorObj K.X (X.{v_1, u_1, u_2} (tensorUnit C c)) i 0 i ⋯))
    (K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      K.ιTensorObj (tensorUnit C c) i 0 i ⋯)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0))
      (K.X i ◁ Iso.inv GradedObject.Monoidal.tensorUnit₀)
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
        (𝟙 (K.X i) ⊗ₘ Iso.hom (tensorUnitIso C c) 0)
        (GradedObject.Monoidal.ιTensorObj K.X (X.{v_1, u_1, u_2} (tensorUnit C c)) i 0 i ⋯)))
    (K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      K.ιTensorObj (tensorUnit C c) i 0 i ⋯)

Tactic:
rw [id_tensorHom, ← whiskerLeft_comp_assoc]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc
-- 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 : I
e_a :
  Eq (α := MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst) ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (CategoryStruct.comp (Y := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0)
      (Iso.inv GradedObject.Monoidal.tensorUnit₀) (Iso.hom (tensorUnitIso C c) 0))
    (Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i)
        (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      (K.tensorObj (tensorUnit C c)).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (K.X i) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
      (K.X i ◁
        CategoryStruct.comp (Y := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0)
          (Iso.inv GradedObject.Monoidal.tensorUnit₀) (Iso.hom (tensorUnitIso C c) 0))
      (GradedObject.Monoidal.ιTensorObj K.X (X.{v_1, u_1, u_2} (tensorUnit C c)) i 0 i ⋯))
    (K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
      K.ιTensorObj (tensorUnit C c) i 0 i ⋯)

Tactic:
congr 2
-- 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 : I
e_a :
  Eq.{v_1 + 1} (α := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom (tensorUnitIso C c) 0 :
      Functor.obj (GradedObject.single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 ⟶
        X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom GradedObject.Monoidal.tensorUnit₀ ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) :
      GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
⊢ Eq (α := MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst) ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (CategoryStruct.comp (Y := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0)
      (Iso.inv GradedObject.Monoidal.tensorUnit₀) (Iso.hom (tensorUnitIso C c) 0))
    (Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))))

Tactic:
rw [← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.GradedObject.Monoidal.tensorUnit₀, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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 : I
e_a :
  Eq (α := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom
      (if hi : Eq.{u_2 + 1} (α := I) 0 0 then
        GradedObject.singleObjApplyIsoOfEq 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 hi ≪≫
          Iso.symm (singleObjXIsoOfEq c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 hi)
      else { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Iso.hom GradedObject.Monoidal.tensorUnit₀ ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))))
⊢ Eq.{v_1 + 1} (α := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom (tensorUnitIso C c) 0 :
      Functor.obj (GradedObject.single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 ⟶
        X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom GradedObject.Monoidal.tensorUnit₀ ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) :
      GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)

Tactic:
dsimp [tensorUnitIso]

Premises used: HomologicalComplex.tensorUnitIso
-- 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 : I
e_a :
  Eq (α := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom
      (GradedObject.singleObjApplyIsoOfEq 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 ⋯ ≪≫
        Iso.symm (singleObjXIsoOfEq c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 ⋯)))
    (Iso.hom GradedObject.Monoidal.tensorUnit₀ ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))))
⊢ Eq (α := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom
      (if hi : Eq.{u_2 + 1} (α := I) 0 0 then
        GradedObject.singleObjApplyIsoOfEq 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 hi ≪≫
          Iso.symm (singleObjXIsoOfEq c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 hi)
      else { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Iso.hom GradedObject.Monoidal.tensorUnit₀ ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))))

Tactic:
rw [dif_pos rfl]

Premises used: dif_pos, 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
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 : I
⊢ Eq (α := GradedObject.Monoidal.tensorUnit.{u_2, v_1, u_1} (I := I) 0 ⟶ X.{v_1, u_1, u_2} (tensorUnit C c) 0)
    (Iso.hom
      (GradedObject.singleObjApplyIsoOfEq 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 ⋯ ≪≫
        Iso.symm (singleObjXIsoOfEq c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst)) 0 ⋯)))
    (Iso.hom GradedObject.Monoidal.tensorUnit₀ ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))))

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
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
pos :
  ∀ (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)
neg :
  ∀ (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)
⊢ 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:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- 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 :
  Eq (α := K.X i ⟶ (K.tensorObj (tensorUnit C c)).X j)
    (Iso.inv (ρ_ (K.X i)) ≫
        K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          mapBifunctor.d₁ K (tensorUnit C c) (curriedTensor C) c i 0 j :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X 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 ⋯ :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X 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 [rightUnitor'_inv, assoc, mapBifunctor.d_eq,
      Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
      tensor_unit_d₂, comp_zero, add_zero]

Premises used: HomologicalComplex.rightUnitor'_inv, HomologicalComplex.mapBifunctor.ι_D₂, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, HomologicalComplex.tensor_unit_d₂, HomologicalComplex.mapBifunctor.d_eq, CategoryTheory.Preadditive.comp_add, HomologicalComplex.mapBifunctor.ι_D₁, add_zero
-- 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
⊢ c.π c c (j, 0) = j

Tactic:
simp
-- 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 (β :=
          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 ⋯
⊢ Eq (α := K.X i ⟶ (K.tensorObj (tensorUnit C c)).X j)
    (Iso.inv (ρ_ (K.X i)) ≫
        K.X i ◁ Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
          mapBifunctor.d₁ K (tensorUnit C c) (curriedTensor C) c i 0 j :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X 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 ⋯ :
      K.X i ⟶ (K.tensorObj (tensorUnit C c)).X j)

Tactic:
rw [mapBifunctor.d₁_eq _ _ _ _ hij _ _ (by simp)]

Premises used: HomologicalComplex.mapBifunctor.d₁_eq