awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₁.π c₂ c (c₁.prev i₁, i₂) = j'
⊢ c.Rel (c₁.π c₂ c (c₁.prev i₁, i₂)) (c₁.π c₂ c (i₁, i₂))

Tactic:
exact ComplexShape.rel_π₁ c₂ c h₃ i₂

Premises used: ComplexShape.rel_π₁
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
neg :
  HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map 0) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0
neg₁ :
  HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app 0 (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0
neg₂ :
  HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (0 ≫ (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0
neg₃ :
  HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂)) 0 = 0
neg₄ neg₅ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') 0 0
⊢ HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0

Tactic:
rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]

Premises used: CategoryTheory.Functor.map_zero, smul_zero, Homotopy.zero, CategoryTheory.Limits.zero_app, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
rw : c₁.π c₂ c (i₁, i₂') = c₁.π c₂ c (i₁', i₂)
rw₁ : c.next (c₁.π c₂ c (i₁, i₂)) = c₁.π c₂ c (i₁', i₂)
rw₂ rw₃ : c₁.π c₂ c (i₁', i₂) = c₁.π c₂ c (i₁', i₂)
⊢ c₁.π c₂ c (i₁, i₂') = j

Tactic:
rw [← hj, ← ComplexShape.next_π₂ c₁ c i₁ hi₂, ComplexShape.next_π₁ c₂ c hi₁ i₂]

Premises used: ComplexShape.next_π₁, ComplexShape.next_π₂
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
⊢ c₁.π c₂ c (i₁, i₂') = j

Tactic:
have hj' : ComplexShape.π c₁ c₂ c ⟨i₁, i₂'⟩ = j := by
    rw [← hj, ← ComplexShape.next_π₂ c₁ c i₁ hi₂, ComplexShape.next_π₁ c₂ c hi₁ i₂]
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
rw : c.next (c₁.π c₂ c (i₁', i₂)) = c.next j
rw₁ rw₂ : c.next j = c.next j
⊢ c₁.π c₂ c (i₁', i₂') = c.next j

Tactic:
rw [← c.next_eq' (ComplexShape.rel_π₂ c₁ c i₁' hi₂), hj]

Premises used: ComplexShape.rel_π₂, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
    CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
        (Hom.f (mapBifunctorMap f₁ f₂ F c) j) =
      K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫
        (HAdd.hAdd (α := X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) (β :=
            X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j)
            (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) (c.next j)) (d (K₁.mapBifunctor K₂ F c) j (c.next j))
                (hom₁ h₁ f₂ F c (c.next j) j) :
              X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j)
            (CategoryStruct.comp (Y := X (L₁.mapBifunctor L₂ F c) (c.prev j))
                (hom₁ h₁ f₂ F c j (c.prev j) : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) (c.prev j))
                (d (L₁.mapBifunctor L₂ F c) (c.prev j) j :
                  X (L₁.mapBifunctor L₂ F c) (c.prev j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
              X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) +
          Hom.f (mapBifunctorMap f₁' f₂ F c) j)
⊢ Hom.f (mapBifunctorMap f₁ f₂ F c) j =
    HAdd.hAdd (α := X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) (β :=
        X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j)
        (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) (c.next j)) (d (K₁.mapBifunctor K₂ F c) j (c.next j))
            (hom₁ h₁ f₂ F c (c.next j) j) :
          X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j)
        (CategoryStruct.comp (Y := X (L₁.mapBifunctor L₂ F c) (c.prev j))
            (hom₁ h₁ f₂ F c j (c.prev j) : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) (c.prev j))
            (d (L₁.mapBifunctor L₂ F c) (c.prev j) j :
              X (L₁.mapBifunctor L₂ F c) (c.prev j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
          X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) +
      Hom.f (mapBifunctorMap f₁' f₂ F c) j

Tactic:
ext i₁ i₂ h
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
X Y : D
a b d : X ⟶ Y
⊢ a + b = a + d + (b + -d)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)

Tactic:
have : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d →
      a + b = c + d + (e + f) := by rintro X Y a b _ d _ _ rfl rfl rfl; abel
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
rw : c₁.π c₂ c (c₁.next i₁, i₂) = c.next (c₁.π c₂ c (i₁, i₂))
rw₁ rw₂ : c₁.π c₂ c (c₁.next i₁, i₂) = c₁.π c₂ c (c₁.next i₁, i₂)
⊢ c₁.π c₂ c (c₁.next i₁, i₂) = c.next j

Tactic:
rw [← h, ComplexShape.next_π₁ c₂ c h₃]

Premises used: ComplexShape.next_π₁
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
rw : c.prev (c₁.π c₂ c (i₁, i₂)) = c.prev j
rw₁ rw₂ : c.prev j = c.prev j
⊢ c₁.π c₂ c (c₁.prev i₁, i₂) = c.prev j

Tactic:
rw [← ComplexShape.prev_π₁ c₂ c h₃, h]

Premises used: ComplexShape.prev_π₁
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j) (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
          HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂) c
            (c₁.prev i₁) i₂ j) =
    -CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j)

Tactic:
comm₁_aux h₁ f₂ F c h₃ h₄ j h

Premises used: HomologicalComplex₂.toGradedObject, CategoryTheory.Limits.colimit, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j) (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
          HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂) c
            (c₁.prev i₁) i₂ j) =
    -CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j)

Tactic:
exact comm₁_aux h₁ f₂ F c h₃ h₄ j h

Premises used: HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
neg :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
⊢ HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) (c.prev j))
        (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
        (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ (c.prev j)) ≫
      HomologicalComplex₂.D₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂) c (c.prev j) j =
    -CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j)

Tactic:
rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp,
        smul_zero, zero_comp, zero_eq_neg]

Premises used: zero_eq_neg, CategoryTheory.Functor.map_zero, smul_zero, Homotopy.zero, CategoryTheory.Limits.zero_app, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next j)
rw : c.next (c₁.π c₂ c (i₁, i₂)) = c.next j
rw₁ rw₂ : c.next j = c.next j
⊢ c₁.π c₂ c (i₁, c₂.next i₂) = c.next j

Tactic:
rw [← ComplexShape.next_π₂ c₁ c i₁ h₄, h]

Premises used: ComplexShape.next_π₂