awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p_1 : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p_1 b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p_1 = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
p : ℤ
hα :
  Cochain.v ((Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯) p (p + 1) ⋯ =
    (↑(cocycle₁' sq hsq) : Cochain B X 1).v p (p + 1) ⋯
⊢ Cochain.v (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)) p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯
have hα₁ : π.f p ≫ α.v p p sorry ≫ K.d p (p + 1) ≫ ι.f (p + 1) - B.d p (p + 1) ≫ π.f (p + 1) ≫ α.v (p + 1) (p + 1) sorry ≫ ι.f (p + 1) =
  HSub.hSub (α := B.X p ⟶ X.X (p + 1)) ((hsq p).l ≫ X.d p (p + 1)) (B.d p (p + 1) ≫ CommSq.LiftStruct.l (hsq (p + 1)))
Tactic: simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v, Cochain.comp_zero_cochain_v,
              δ_zero_cochain_v, Preadditive.sub_comp, Category.assoc, Preadditive.comp_sub,
              HomologicalComplex.Hom.comm_assoc, cocycle₁', Cocycle.mk_coe, Cochain.ofHoms_v,
              HomologicalComplex.eval_obj, HomologicalComplex.eval_map] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
⊢ i ≫ l.homOf = t
have h : ∀ (n : ℤ), (i ≫ l.homOf).f n = t.f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ (i ≫ l.homOf).f n = t.f n
have h₁ : i.f n ≫ π.f n = 0
Tactic: have h₁ : i.f n ≫ π.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
h₁ : i.f n ≫ π.f n = 0
⊢ (i ≫ l.homOf).f n = t.f n
have h₂ : CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n) i ≫ (hsq n).l =
  CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n) t
Tactic: have h₂ := (hsq n).fac_left
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
⊢ l.homOf ≫ p = b
have h : ∀ (n : ℤ), (l.homOf ≫ p).f n = b.f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ (l.homOf ≫ p).f n = b.f n
have this : ι.f n ≫ p.f n = 0
Tactic: have : ι.f n ≫ p.f n = 0 := by
          simp [← HomologicalComplex.comp_f, 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
⊢ 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 pos : ∀ (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
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 (Functor.flip (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) (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
have neg : ∀ (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
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 (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 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
Tactic: by_cases h₂ : ComplexShape.π c c c (c.next i₁, 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 (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
⊢ 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 : ∀ (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
Tactic: by_cases h₂ : ComplexShape.π c c c (c.next i₁, 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 (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 pos : 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) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (c.ε₁ c c (i₁, i₂))
    (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (d (tensorUnit C c) i₁ (c.next i₁))) (K.X i₂) ≫
      ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
  0
Tactic: rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, 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 (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
pos :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (d (tensorUnit C c) i₁ (c.next i₁))) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    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
have pos₁ : 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) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (c.ε₁ c c (i₁, i₂))
    (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) 0) (K.X i₂) ≫
      ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
  0
Tactic: rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, 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 (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
pos :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (d (tensorUnit C c) i₁ (c.next i₁))) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₁ :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) 0) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    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
have pos₂ : 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) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (c.ε₁ c c (i₁, i₂))
    (NatTrans.app 0 (K.X i₂) ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
  0
Tactic: rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, 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 (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
pos :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (d (tensorUnit C c) i₁ (c.next i₁))) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₁ :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) 0) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₂ :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app 0 (K.X i₂) ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    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
have pos₃ : 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) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (c.ε₁ c c (i₁, i₂)) (0 ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
  0
Tactic: rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, 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 (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
pos :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) (d (tensorUnit C c) i₁ (c.next i₁))) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₁ :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app (CategoryTheory.Functor.map (curriedTensor C) 0) (K.X i₂) ≫
        ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₂ :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂))
      (NatTrans.app 0 (K.X i₂) ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    0
pos₃ :
  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) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (c.ε₁ c c (i₁, i₂)) (0 ≫ ιMapBifunctor (tensorUnit C c) K (curriedTensor C) c (c.next i₁) i₂ j h₂) =
    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
have pos₄ : 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) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (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_app, zero_comp, smul_zero]