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₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
pos :
  ∀ (h₂ : c.π c c (c.next i₁, i₂) = j),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0
neg :
  ∀ (h₂ : ¬c.π c c (c.next i₁, i₂) = j),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0

Tactic:
by_cases h₂ : ComplexShape.π c c c (c.next i₁, i₂) = j

Premises used: Prod.mk, ComplexShape.next, ComplexShape.π
-- 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₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : ¬c.π c c (c.next i₁, i₂) = j
neg neg₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    0 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0

Tactic:
rw [mapBifunctor.d₁_eq_zero' _ _ _ _ h₁ _ _ h₂]

Premises used: HomologicalComplex.mapBifunctor.d₁_eq_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₁ i₂ j : I
h₁ : ¬c.Rel i₁ (c.next i₁)
neg neg₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    0 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0

Tactic:
rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁]

Premises used: HomologicalComplex.mapBifunctor.d₁_eq_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₁)
⊢ GradedObject.HasTensor.{u_2, v_1, u_1} K.X (X.{v_1, u_1, u_2} (tensorUnit C c))

Tactic:
GradedObject.hasTensor_of_iso (Iso.refl _) (tensorUnitIso C c)

Premises used: HomologicalComplex.tensorUnitIso, CategoryTheory.Iso.refl, CategoryTheory.GradedObject.hasTensor_of_iso
-- 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₁)
⊢ K.HasTensor (tensorUnit C c)

Tactic:
inferInstanceAs (GradedObject.HasTensor K.X (tensorUnit C c).X)

Premises used: _private.0.HomologicalComplex.instHasTensorTensorUnit_1._proof_1
-- 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₂ j : I
pos :
  ∀ (h₁ : c.Rel i₂ (c.next i₂)),
    Eq (α :=
      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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0
neg :
  ∀ (h₁ : ¬c.Rel i₂ (c.next i₂)),
    Eq (α :=
      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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0
⊢ Eq (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0

Tactic:
by_cases h₁ : c.Rel i₂ (c.next i₂)

Premises used: ComplexShape.next, 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₁ i₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
pos :
  ∀ (h₂ : c.π c c (i₁, c.next i₂) = j),
    Eq (α :=
      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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0
neg :
  ∀ (h₂ : ¬c.π c c (i₁, c.next i₂) = j),
    Eq (α :=
      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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0
⊢ Eq (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0

Tactic:
by_cases h₂ : ComplexShape.π c c c (i₁, c.next i₂) = j

Premises used: Prod.mk, ComplexShape.next, ComplexShape.π
-- 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₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
h₂ : c.π c c (i₁, c.next i₂) = j
pos :
  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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (c.ε₂ c c (i₁, i₂))
      (CategoryTheory.Functor.map (Functor.obj (curriedTensor C) (K.X i₁)) (d (tensorUnit C c) i₂ (c.next i₂)) ≫
        K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c i₁ (c.next i₂) j h₂) =
    0
pos₁ :
  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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (c.ε₂ c c (i₁, i₂))
      (CategoryTheory.Functor.map (Functor.obj (curriedTensor C) (K.X i₁)) 0 ≫
        K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c i₁ (c.next i₂) j h₂) =
    0
pos₂ :
  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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (c.ε₂ c c (i₁, i₂)) (0 ≫ K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c i₁ (c.next i₂) j h₂) =
    0
pos₃ :
  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) i₂) ⟶
        X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
      (c.ε₂ c c (i₁, i₂)) 0 =
    0
pos₄ pos₅ :
  Eq.{v_1 + 1} (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    0 0
⊢ Eq (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0

Tactic:
rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero,
        zero_comp, smul_zero]

Premises used: HomologicalComplex.single_obj_d, CategoryTheory.Functor.map_zero, smul_zero, HomologicalComplex.mapBifunctor.d₂_eq, CategoryTheory.Limits.zero_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
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₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
h₂ : ¬c.π c c (i₁, c.next i₂) = j
neg neg₁ :
  Eq.{v_1 + 1} (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    0 0
⊢ Eq (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0

Tactic:
rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂]

Premises used: HomologicalComplex.mapBifunctor.d₂_eq_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₁ i₂ j : I
h₁ : ¬c.Rel i₂ (c.next i₂)
neg neg₁ :
  Eq.{v_1 + 1} (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    0 0
⊢ Eq (α :=
    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) i₂) ⟶
      X (K.mapBifunctor (tensorUnit C c) (curriedTensor C) c) j)
    (mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j) 0

Tactic:
rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁]

Premises used: HomologicalComplex.mapBifunctor.d₂_eq_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 : I
dsimp :
  Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)
    (CategoryStruct.comp (Y :=
        GradedObject.Monoidal.tensorObj.{u_2, v_1, u_1}
          (Functor.obj (GradedObject.single₀ I) (MonoidalCategoryStruct.tensorUnit.{v_1, u_1} C (𝒞 := inst))) K.X i)
        (Iso.inv (GradedObject.Monoidal.leftUnitor K.X) i)
        (GradedObject.Monoidal.tensorHom (Iso.hom (tensorUnitIso C c)) (𝟙 K.X) i) :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)
    (Iso.inv (λ_ (K.X 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 ⋯ :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)
    (Iso.inv K.leftUnitor' i : K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)
    (Iso.inv (λ_ (K.X 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 ⋯ :
      K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)

Tactic:
dsimp [leftUnitor']

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

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GradedObject.Monoidal.leftUnitor_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 (Functor.flip (curriedTensor C)) X₂)
i : I
dsimp :
  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 ⋯)
⊢ 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:
dsimp