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

Tactic:
rw [tensorHom_id, ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.tensorHom_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 (Functor.flip (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) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))
        (K.X i) ⟶
      (tensorObj (tensorUnit C c) K).X i)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (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) ▷
        K.X i)
      (GradedObject.Monoidal.ιTensorObj (X.{v_1, u_1, u_2} (tensorUnit C c)) K.X 0 i i ⋯))
    (Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
      ιTensorObj (tensorUnit C c) K 0 i 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 (Functor.flip (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 (Functor.flip (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 (Functor.flip (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 (Functor.flip (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 (Functor.flip (curriedTensor C)) X₂)
i j : I
pos :
  ∀ (hij : c.Rel i j),
    Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
      (Iso.inv K.leftUnitor' i ≫ (tensorObj (tensorUnit C c) K).d i j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
      (K.d i j ≫ Iso.inv K.leftUnitor' j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
neg :
  ∀ (hij : ¬c.Rel i j),
    Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
      (Iso.inv K.leftUnitor' i ≫ (tensorObj (tensorUnit C c) K).d i j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
      (K.d i j ≫ Iso.inv K.leftUnitor' j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (Iso.inv K.leftUnitor' i ≫ (tensorObj (tensorUnit C c) K).d i j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (K.d i j ≫ Iso.inv K.leftUnitor' j : K.X i ⟶ (tensorObj (tensorUnit C c) K).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 (Functor.flip (curriedTensor C)) X₂)
i j : I
hij : c.Rel i j
pos :
  Eq (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (Iso.inv (λ_ (K.X i)) ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
          mapBifunctor.d₂ (tensorUnit C c) K (curriedTensor C) c 0 i j :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (K.d i j ≫
        Iso.inv (λ_ (K.X j)) ≫
          Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X j ≫
            ιTensorObj (tensorUnit C c) K 0 j j ⋯ :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (Iso.inv K.leftUnitor' i ≫ (tensorObj (tensorUnit C c) K).d i j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (K.d i j ≫ Iso.inv K.leftUnitor' j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)

Tactic:
simp only [leftUnitor'_inv, assoc, mapBifunctor.d_eq,
      Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
      unit_tensor_d₁, comp_zero, zero_add]

Premises used: HomologicalComplex.mapBifunctor.ι_D₂, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, zero_add, HomologicalComplex.mapBifunctor.d_eq, HomologicalComplex.leftUnitor'_inv, CategoryTheory.Preadditive.comp_add, HomologicalComplex.mapBifunctor.ι_D₁, HomologicalComplex.unit_tensor_d₁
-- 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 (Functor.flip (curriedTensor C)) X₂)
i j : I
hij : c.Rel i j
⊢ c.π c c (0, j) = 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 (Functor.flip (curriedTensor C)) X₂)
i j : I
hij : c.Rel i j
pos :
  Iso.inv (λ_ (K.X i)) ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
        HSMul.hSMul (β :=
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
              (K.X i) ⟶
            X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
          (c.ε₂ c c (0, i))
          (CategoryTheory.Functor.map (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) 0)) (K.d i j) ≫
            ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫
      Iso.inv (λ_ (K.X j)) ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X j ≫
          ιTensorObj (tensorUnit C c) K 0 j j ⋯
⊢ Eq (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (Iso.inv (λ_ (K.X i)) ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
          mapBifunctor.d₂ (tensorUnit C c) K (curriedTensor C) c 0 i j :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (K.d i j ≫
        Iso.inv (λ_ (K.X j)) ≫
          Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X j ≫
            ιTensorObj (tensorUnit C c) K 0 j j ⋯ :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)

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

Premises used: HomologicalComplex.mapBifunctor.d₂_eq
-- 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 (Functor.flip (curriedTensor C)) X₂)
i j : I
hij : c.Rel i j
pos :
  Iso.inv (λ_ (K.X i)) ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
        HSMul.hSMul (β :=
          MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (X.{v_1, u_1, u_2} (tensorUnit C c) 0) (K.X i) ⟶
            X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
          (c.ε 0)
          (X.{v_1, u_1, u_2} (tensorUnit C c) 0 ◁ K.d i j ≫
            ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫
      Iso.inv (λ_ (K.X j)) ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X j ≫
          ιTensorObj (tensorUnit C c) K 0 j j ⋯
⊢ Iso.inv (λ_ (K.X i)) ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
        HSMul.hSMul (β :=
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) 0))
              (K.X i) ⟶
            X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
          (c.ε₂ c c (0, i))
          (CategoryTheory.Functor.map (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) 0)) (K.d i j) ≫
            ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫
      Iso.inv (λ_ (K.X j)) ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X j ≫
          ιTensorObj (tensorUnit C c) K 0 j 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 (Functor.flip (curriedTensor C)) X₂)
i j : I
hij : c.Rel i j
⊢ Iso.inv (λ_ (K.X i)) ≫
      Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X i ≫
        HSMul.hSMul (β :=
          MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := inst) (X.{v_1, u_1, u_2} (tensorUnit C c) 0) (K.X i) ⟶
            X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
          (c.ε 0)
          (X.{v_1, u_1, u_2} (tensorUnit C c) 0 ◁ K.d i j ≫
            ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c 0 j j ⋯) =
    K.d i j ≫
      Iso.inv (λ_ (K.X j)) ≫
        Iso.inv (singleObjXSelf c 0 (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) ▷ K.X j ≫
          ιTensorObj (tensorUnit C c) K 0 j j ⋯

Tactic:
simp only [ComplexShape.ε_zero, one_smul, ← whisker_exchange_assoc,
      id_whiskerLeft, assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_whiskerLeft, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, one_smul, ComplexShape.ε_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 (Functor.flip (curriedTensor C)) X₂)
i j : I
hij : ¬c.Rel i j
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (Iso.inv K.leftUnitor' i ≫ (tensorObj (tensorUnit C c) K).d i j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)
    (K.d i j ≫ Iso.inv K.leftUnitor' j : K.X i ⟶ (tensorObj (tensorUnit C c) K).X j)

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

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape