Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ HomologicalComplex₂.total.map
        (K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
            x).hom
        (ComplexShape.up ℤ) ≫
      HomologicalComplex₂.total.map
          ((HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom)
          (ComplexShape.up ℤ) ≫
        ((x * y).negOnePow •
          HomologicalComplex₂.total.map
              ((HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂))
              (ComplexShape.up ℤ) ≫
            (((HomologicalComplex₂.shiftFunctor₁ D x).obj
                      (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                        K₂)).totalShift₂Iso
                  y).hom ≫
              (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) y).map
                  ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                          K₂).totalShift₁Iso
                      x).hom ≫
                (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app
                  ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).total
                    (ComplexShape.up ℤ))) =
    (x * y).negOnePow •
      HomologicalComplex₂.total.map
          (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
              y).hom
          (ComplexShape.up ℤ) ≫
        ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                      ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁)).obj
                  K₂).totalShift₂Iso
              y).hom ≫
          (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
              (HomologicalComplex₂.total.map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom
                (ComplexShape.up ℤ)) ≫
            (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
                ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                        K₂).totalShift₁Iso
                    x).hom ≫
              (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app (K₁.mapBifunctor K₂ F)

Tactic:
← HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ HomologicalComplex₂.total.map
        (K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
            x).hom
        (ComplexShape.up ℤ) ≫
      HomologicalComplex₂.total.map
          ((HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom)
          (ComplexShape.up ℤ) ≫
        ((x * y).negOnePow •
          HomologicalComplex₂.total.map
              ((HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂))
              (ComplexShape.up ℤ) ≫
            (((HomologicalComplex₂.shiftFunctor₁ D x).obj
                      (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                        K₂)).totalShift₂Iso
                  y).hom ≫
              (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) y).map
                  ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                          K₂).totalShift₁Iso
                      x).hom ≫
                (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app
                  ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).total
                    (ComplexShape.up ℤ))) =
    (x * y).negOnePow •
      HomologicalComplex₂.total.map
          (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
              y).hom
          (ComplexShape.up ℤ) ≫
        HomologicalComplex₂.total.map
            ((HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom)
            (ComplexShape.up ℤ) ≫
          (((HomologicalComplex₂.shiftFunctor₁ D x).obj
                    (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                      K₂)).totalShift₂Iso
                y).hom ≫
            (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
                ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                        K₂).totalShift₁Iso
                    x).hom ≫
              (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app (K₁.mapBifunctor K₂ F)