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
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)
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))
        0 :
      (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)
neg₁ neg₂ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j) 0 0
⊢ 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)

Tactic:
rw [zero₁ _ _ _ _ _ _ h₅, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.mapBifunctorMapHomotopy.zero₁
-- 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₂)
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))
        (0 :
          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)
neg₁ neg₂ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j) 0 0
⊢ 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)

Tactic:
rw [HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h₄, zero_comp]

Premises used: HomologicalComplex₂.d₂_eq_zero, 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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this_1 : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this_2 : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this_3 : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
⊢ Eq (α := Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c) (L₁.mapBifunctor L₂ F c))
    (mapBifunctorMap f₁ f₂ F c)
    (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
      (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c) (K₂.mapBifunctor K₁ F.flip c))
      (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
          (mapBifunctorMap f₂ f₁ F.flip c :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
              (L₂.mapBifunctor L₁ F.flip c))
          (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
              (L₁.mapBifunctor L₂ F c)) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
          (L₁.mapBifunctor L₂ F c)))

Tactic:
simp
-- 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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this_1 : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this_2 : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this_3 : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
⊢ Eq (α := Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c) (L₁.mapBifunctor L₂ F c))
    (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
      (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c) (K₂.mapBifunctor K₁ F.flip c))
      (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
          (mapBifunctorMap f₂' f₁ F.flip c :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
              (L₂.mapBifunctor L₁ F.flip c))
          (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
              (L₁.mapBifunctor L₂ F c)) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
          (L₁.mapBifunctor L₂ F c)))
    (mapBifunctorMap f₁ f₂' F c)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
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₁).PreservesZeroMorphisms
x : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
i j : ℤ
h : (ComplexShape.up ℤ).Rel i j
i_1 : ℤ
⊢ 𝟙 ((F.obj (K₁.X (i + x))).obj (K₂.X i_1)) ≫
      HSMul.hSMul (β := (F.obj (K₁.X (i + x))).obj (K₂.X i_1) ⟶ (F.obj (K₁.X (j + x))).obj (K₂.X i_1)) x.negOnePow
        (NatTrans.app (F.map (K₁.d (i + x) (j + x))) (K₂.X i_1)) =
    (F.map (HSMul.hSMul (β := K₁.X (i + x) ⟶ K₁.X (j + x)) x.negOnePow (K₁.d (i + x) (j + x)))).app (K₂.X i_1) ≫
      𝟙 ((F.obj (K₁.X (j + x))).obj (K₂.X i_1))

Tactic:
simp only [Linear.comp_units_smul, id_comp, Functor.map_units_smul,
      NatTrans.app_units_zsmul, comp_id]

Premises used: CategoryTheory.Linear.comp_units_smul, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_units_smul, CategoryTheory.NatTrans.app_units_zsmul, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
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₁).PreservesZeroMorphisms
x : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).HasMapBifunctor K₂ F

Tactic:
HomologicalComplex₂.hasTotal_of_iso (mapBifunctorHomologicalComplexShift₁Iso K₁ K₂ F x).symm _

Premises used: CategoryTheory.Iso.symm, HomologicalComplex₂.hasTotal_of_iso, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
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₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
i j : ℤ
h : (ComplexShape.up ℤ).Rel i j
i_1 : ℤ
⊢ 𝟙 ((F.obj (K₁.X i)).obj (K₂.X (i_1 + y))) ≫ (F.map (K₁.d i j)).app (K₂.X (i_1 + y)) =
    (F.map (K₁.d i j)).app (K₂.X (i_1 + y)) ≫ 𝟙 ((F.obj (K₁.X j)).obj (K₂.X (i_1 + y)))

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
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₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
⊢ K₁.HasMapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F

Tactic:
HomologicalComplex₂.hasTotal_of_iso (mapBifunctorHomologicalComplexShift₂Iso K₁ K₂ F y).symm _

Premises used: CategoryTheory.Iso.symm, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso, HomologicalComplex₂.hasTotal_of_iso
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
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₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₂ m : ℤ
hm₂ : m₂ = n₂ + y
hm : m = n + y
⊢ n₁ + m₂ = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} 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₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₂ m : ℤ
hm₂ : m₂ = n₂ + y
hm : m = n + y
⊢ Hom.f (Hom.f (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y)) n₁) n₂ ≫
      HSMul.hSMul (β :=
        X
            (X
              (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              n₁)
            n₂ ⟶
          X
            (Functor.obj (shiftFunctor D y)
              (HomologicalComplex₂.total
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂)
                (ComplexShape.up ℤ)))
            n)
        (n₁ * y).negOnePow
        (Iso.hom
            (HomologicalComplex₂.shiftFunctor₂XXIso
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂)
              n₁ n₂ y m₂ hm₂) ≫
          HomologicalComplex₂.ιTotal
              (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                K₂)
              (ComplexShape.up ℤ) n₁ m₂ m ⋯ ≫
            Iso.inv
              (shiftFunctorObjXIso
                (HomologicalComplex₂.total
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
                  (ComplexShape.up ℤ))
                y n m hm)) =
    HSMul.hSMul (β := (F.obj (K₁.X n₁)).obj (K₂.X (n₂ + y)) ⟶ X (K₁.mapBifunctor K₂ F) (n + y)) (n₁ * y).negOnePow
      ((F.obj (K₁.X n₁)).map (XIsoOfEq K₂ ⋯).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ Iso.inv (XIsoOfEq (K₁.mapBifunctor K₂ F) ⋯))

Tactic:
simp [HomologicalComplex₂.ιTotal, HomologicalComplex₂.shiftFunctor₂XXIso,
    HomologicalComplex.XIsoOfEq, eqToHom_map]

Premises used: HomologicalComplex₂.ιTotal, CategoryTheory.eqToHom_map, HomologicalComplex.XIsoOfEq, HomologicalComplex₂.shiftFunctor₂XXIso
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
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
x y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
a b : ℤ
⊢ Eq.{v_3 + 1} (α := (F.obj (K₁.X (a + x))).obj (K₂.X (b + y)) ⟶ (F.obj (K₁.X (a + x))).obj (K₂.X (b + y)))
    ((𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y)))) ≫
      𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))))
    (𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))))

Tactic:
simp only [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
      (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁) K₂)
      (obj (obj F.map₂CochainComplex K₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₂))
    (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n)) K₂)
    (Iso.hom (K₁.mapBifunctorShift₂Iso K₂ F n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
      (obj (obj F.map₂CochainComplex K₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₂)
      (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁) K₂))
    (NatTrans.app (Iso.inv (commShiftIso (obj F.map₂CochainComplex K₁) n)) K₂)
    (Iso.inv (K₁.mapBifunctorShift₂Iso K₂ F n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
w :
  ∀ (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ) (d : ℤ),
    Eq (α :=
      X (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁) K₂) d ⟶
        X (obj (obj F.map₂CochainComplex L₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₂) d)
      (Hom.f
        (NatTrans.app
          (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n) ≫
            whiskerRight (map F.map₂CochainComplex f) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
          K₂)
        d)
      (Hom.f
        (NatTrans.app
          (whiskerLeft (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) (map F.map₂CochainComplex f) ≫
            Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n))
          K₂)
        d)
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_2, u_2, 0} C₂ ℤ ⥤ CochainComplex.{v_3, u_3, 0} D ℤ)
      (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁)
      (obj F.map₂CochainComplex L₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
    (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n) ≫
      whiskerRight (map F.map₂CochainComplex f) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
    (whiskerLeft (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) (map F.map₂CochainComplex f) ≫
      Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n))

Tactic:
ext K₂ d

Premises used: HomologicalComplex.d
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
d : ℤ
w :
  Eq (α :=
    X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
      X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y := X (mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)) (d + n))
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n)) K₂) d)
        (Hom.f (mapBifunctorMap f (𝟙 K₂) F (ComplexShape.up ℤ)) (d + n)) :
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
        X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y :=
        X (mapBifunctor L₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
        (Hom.f
          (mapBifunctorMap f (𝟙 (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂)) F (ComplexShape.up ℤ)) d)
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n)) K₂) d) :
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
        X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
⊢ Eq (α :=
    X (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁) K₂) d ⟶
      X (obj (obj F.map₂CochainComplex L₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₂) d)
    (Hom.f
      (NatTrans.app
        (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n) ≫
          whiskerRight (map F.map₂CochainComplex f) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
        K₂)
      d)
    (Hom.f
      (NatTrans.app
        (whiskerLeft (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) (map F.map₂CochainComplex f) ≫
          Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n))
        K₂)
      d)

Tactic:
dsimp