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 (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
⊢ 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
have 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
Tactic: rw [mapBifunctor.d₁_eq_zero' _ _ _ _ h₁ _ _ h₂]
-- 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 (Functor.flip (curriedTensor C)) X₂)
i₁ i₂ j : I
h₁ : ¬c.Rel i₁ (c.next i₁)
⊢ 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
have 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
Tactic: rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁]
-- 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₁ i₂ j : 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
have 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
Tactic: by_cases h₁ : c.Rel i₂ (c.next i₂)
-- 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₁ 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
⊢ 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
have 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
Tactic: by_cases h₁ : c.Rel i₂ (c.next i₂)
-- 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₁ i₂ j : I
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
have 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
Tactic: by_cases h₂ : ComplexShape.π c c c (i₁, c.next i₂) = j
-- 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₁ 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
⊢ 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
have 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
Tactic: by_cases h₂ : ComplexShape.π c c c (i₁, c.next i₂) = j
-- 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₁ i₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
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
have 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
Tactic: rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero,
        zero_comp, smul_zero]
-- 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₁ 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
⊢ 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
have 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
Tactic: rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero,
        zero_comp, smul_zero]
-- 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₁ 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
⊢ 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
have 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
Tactic: rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero,
        zero_comp, smul_zero]
-- 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₁ 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
⊢ 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
have 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
Tactic: rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero,
        zero_comp, smul_zero]
-- 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₁ 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
⊢ 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
have 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
Tactic: rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, single_obj_d, Functor.map_zero,
        zero_comp, smul_zero]
-- 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₁ i₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
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
have 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
Tactic: rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂]
-- 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₁ i₂ j : I
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
have 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
Tactic: rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁]
-- 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 (Functor.flip (curriedTensor C)) X₂)
i : 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)
have 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 sorry :
    K.X i ⟶ (tensorObj (tensorUnit C c) K).X i)
Tactic: dsimp [leftUnitor']