awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ K₁' : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f : K₁ ⟶ K₁'
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
i₂ : I₂
h : c₁.Rel i₁ i₁'
⊢ Eq (α :=
    HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) (i₁, i₂) ⟶
      (F.obj (K₁'.X i₁')).obj (K₂.X i₂))
    ((F.map (f.f i₁)).app (K₂.X i₂) ≫ (F.map (K₁'.d i₁ i₁')).app (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (f.f i₁')).app (K₂.X i₂))

Tactic:
simp only [← NatTrans.comp_app, ← F.map_comp, f.comm]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ K₁' : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f : K₁ ⟶ K₁'
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
⊢ ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      Eq.{v_3 + 1} (α :=
        HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) (i₁, i₂) ⟶
          HomologicalComplex.X (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) i₁) i₂')
        (((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁, i₂) ≫
            HomologicalComplex.d (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) i₁) i₂
              i₂' :
          HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) (i₁, i₂) ⟶
            HomologicalComplex.X (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) i₁) i₂')
        (HomologicalComplex.d (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) i₁) i₂ i₂' ≫
            ((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁, i₂') :
          HomologicalComplex.X (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) i₁) i₂ ⟶
            HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) (i₁, i₂'))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
⊢ HomologicalComplex₂.toGradedObject (obj (obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) =
    ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X

Tactic:
rfl

Premises used: HomologicalComplex₂.toGradedObject, rfl
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j)
    (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)

Tactic:
dif_pos h

Premises used: HomologicalComplex₂.toGradedObject, HomologicalComplex₂.ιTotal, dif_pos, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapObjOrZero, HomologicalComplex₂.ιTotalOrZero, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) ≠ j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j) 0

Tactic:
dif_neg h

Premises used: HomologicalComplex₂.toGradedObject, dif_neg, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapObjOrZero, HomologicalComplex₂.ιTotalOrZero, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
A : D
j : J
f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A)
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) (mapBifunctorDesc f) =
    f i₁ i₂ h

Tactic:
apply HomologicalComplex₂.ι_totalDesc

Premises used: HomologicalComplex₂.ι_totalDesc
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
Y : D
j : J
f g : X (K₁.mapBifunctor K₂ F c) j ⟶ Y
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
    K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ f = K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ g
⊢ f = g

Tactic:
HomologicalComplex₂.total.hom_ext _ h

Premises used: HomologicalComplex₂.total.hom_ext
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
j j' : J
⊢ d (K₁.mapBifunctor K₂ F c) j j' =
    HAdd.hAdd (α := X (K₁.mapBifunctor K₂ F c) j ⟶ X (K₁.mapBifunctor K₂ F c) j') (D₁ K₁ K₂ F c j j')
      (D₂ K₁ K₂ F c j j')

Tactic:
rfl

Premises used: HomologicalComplex.mapBifunctor.D₂, HomologicalComplex.mapBifunctor.D₁, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj, rfl
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (d₁ K₁ K₂ F c i₁ i₂ j) 0

Tactic:
HomologicalComplex₂.d₁_eq_zero _ _ _ _ _ h

Premises used: HomologicalComplex₂.d₁_eq_zero, CategoryTheory.Limits.colimit, HomologicalComplex.mapBifunctor.d₁, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (d₂ K₁ K₂ F c i₁ i₂ j) 0

Tactic:
HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h

Premises used: HomologicalComplex.mapBifunctor.d₂, HomologicalComplex₂.d₂_eq_zero, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
j : J
h' : c₁.π c₂ c (i₁', i₂) ≠ j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (d₁ K₁ K₂ F c i₁ i₂ j) 0

Tactic:
HomologicalComplex₂.d₁_eq_zero' _ _ h _ _ h'

Premises used: HomologicalComplex₂.d₁_eq_zero', CategoryTheory.Limits.colimit, HomologicalComplex.mapBifunctor.d₁, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
j : J
h' : c₁.π c₂ c (i₁, i₂') ≠ j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (d₂ K₁ K₂ F c i₁ i₂ j) 0

Tactic:
HomologicalComplex₂.d₂_eq_zero' _ _ _ h _ h'

Premises used: HomologicalComplex.mapBifunctor.d₂, CategoryTheory.Limits.colimit, HomologicalComplex₂.d₂_eq_zero', CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
j : J
⊢ d₁ K₁ K₂ F c i₁ i₂ j =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (c₁.ε₁ c₂ c (i₁, i₂))
      ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ K₁.ιMapBifunctorOrZero K₂ F c i₁' i₂ j)

Tactic:
HomologicalComplex₂.d₁_eq' _ _ h _ _

Premises used: CategoryTheory.Limits.colimit, HomologicalComplex.mapBifunctor.d₁, CategoryTheory.GradedObject.mapObj, HomologicalComplex₂.d₁_eq'
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
j : J
⊢ d₂ K₁ K₂ F c i₁ i₂ j =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (c₁.ε₂ c₂ c (i₁, i₂))
      ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂' j)

Tactic:
HomologicalComplex₂.d₂_eq' _ _ _ h _

Premises used: HomologicalComplex.mapBifunctor.d₂, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj, HomologicalComplex₂.d₂_eq'
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
j : J
h' : c₁.π c₂ c (i₁', i₂) = j
⊢ d₁ K₁ K₂ F c i₁ i₂ j =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (c₁.ε₁ c₂ c (i₁, i₂))
      ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ K₁.ιMapBifunctor K₂ F c i₁' i₂ j h')

Tactic:
HomologicalComplex₂.d₁_eq _ _ h _ _ h'

Premises used: HomologicalComplex₂.d₁_eq, CategoryTheory.Limits.colimit, HomologicalComplex.mapBifunctor.d₁, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
j : J
h' : c₁.π c₂ c (i₁, i₂') = j
⊢ d₂ K₁ K₂ F c i₁ i₂ j =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j) (c₁.ε₂ c₂ c (i₁, i₂))
      ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ K₁.ιMapBifunctor K₂ F c i₁ i₂' j h')

Tactic:
HomologicalComplex₂.d₂_eq _ _ _ h _ h'

Premises used: HomologicalComplex.mapBifunctor.d₂, CategoryTheory.Limits.colimit, HomologicalComplex₂.d₂_eq, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
j j' : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j')
    (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ D₁ K₁ K₂ F c j j') (d₁ K₁ K₂ F c i₁ i₂ j')

Tactic:
apply HomologicalComplex₂.ι_D₁

Premises used: HomologicalComplex₂.ι_D₁
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : DecidableEq J
j j' : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j')
    (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ D₂ K₁ K₂ F c j j') (d₂ K₁ K₂ F c i₁ i₂ j')

Tactic:
apply HomologicalComplex₂.ι_D₂

Premises used: HomologicalComplex₂.ι_D₂
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₁ : K₁ ⟶ L₁
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : K₁.HasMapBifunctor K₂ F c
inst_10 : L₁.HasMapBifunctor L₂ F c
inst_11 : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) 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))
    ((F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h)

Tactic:
simp [mapBifunctorMap]

Premises used: HomologicalComplex.mapBifunctorMap
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : Category.{v_6, u_4} C₂₃
inst_6 : HasZeroMorphisms.{v_1, u_1} C₁
inst_7 : HasZeroMorphisms.{v_2, u_2} C₂
inst_8 : HasZeroMorphisms.{v_3, u_5} C₃
inst_9 : Preadditive.{v_5, u_3} C₁₂
inst_10 : Preadditive.{v_6, u_4} C₂₃
inst_11 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
F : C₁ ⥤ CategoryTheory.Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ CategoryTheory.Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
inst_12 : F₁₂.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_14 : G.Additive
inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst_16 : G₂₃.PreservesZeroMorphisms
inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_18 : F.PreservesZeroMorphisms
inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst_20 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst_21 : TotalComplexShape c₁ c₂ c₁₂
inst_22 : TotalComplexShape c₁₂ c₃ c₄
inst_23 : TotalComplexShape c₂ c₃ c₂₃
inst_24 : TotalComplexShape c₁ c₂₃ c₄
inst_25 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_26 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_27 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
⊢ (((GradedObject.mapBifunctor F₁₂ ι₁ ι₂).obj K₁.X).obj K₂.X).HasMap (c₁.π c₂ c₁₂)

Tactic:
inferInstanceAs (HasMapBifunctor K₁ K₂ F₁₂ c₁₂)

Premises used: _private.0.HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ._proof_1