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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
p q : ℤ
this :
  (K₁.mapBifunctorShift₁Iso ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂) F p ≪≫
        (shiftFunctor (CochainComplex D ℤ) p).mapIso (K₁.mapBifunctorShift₂Iso K₂ F q)).hom =
    ((p * q).negOnePow •
        ((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁).mapBifunctorShift₂Iso K₂ F q ≪≫
          (shiftFunctor (CochainComplex D ℤ) q).mapIso (K₁.mapBifunctorShift₁Iso K₂ F p) ≪≫
            (shiftFunctorComm (CochainComplex D ℤ) p q).app (K₁.mapBifunctor K₂ F)).hom
⊢ (commShiftIso (F.map₂CochainComplex.obj ((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁)) q).hom.app K₂ ≫
      (shiftFunctor (CochainComplex D ℤ) q).map ((commShiftIso (F.map₂CochainComplex.flip.obj K₂) p).hom.app K₁) =
    (commShiftIso (F.map₂CochainComplex.flip.obj ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂)) p).hom.app K₁ ≫
      (shiftFunctor (CochainComplex D ℤ) p).map ((commShiftIso (F.map₂CochainComplex.obj K₁) q).hom.app K₂) ≫
        (shiftComm ((F.map₂CochainComplex.obj K₁).obj K₂) p q).inv ≫
          (↑(CommShift₂Setup.int.ε p q)).app
            ((shiftFunctor (CochainComplex D ℤ) q).obj
              ((shiftFunctor (CochainComplex D ℤ) p).obj ((F.map₂CochainComplex.obj K₁).obj K₂)))

Tactic:
dsimp at this

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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
p q : ℤ
this :
  (K₁.mapBifunctorShift₁Iso ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂) F p).hom ≫
      (shiftFunctor (CochainComplex D ℤ) p).map (K₁.mapBifunctorShift₂Iso K₂ F q).hom =
    (p * q).negOnePow •
      (((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁).mapBifunctorShift₂Iso K₂ F q).hom ≫
        (shiftFunctor (CochainComplex D ℤ) q).map (K₁.mapBifunctorShift₁Iso K₂ F p).hom ≫
          (shiftFunctorComm (CochainComplex D ℤ) p q).hom.app (K₁.mapBifunctor K₂ F)
⊢ (commShiftIso (F.map₂CochainComplex.obj ((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁)) q).hom.app K₂ ≫
      (shiftFunctor (CochainComplex D ℤ) q).map ((commShiftIso (F.map₂CochainComplex.flip.obj K₂) p).hom.app K₁) =
    (commShiftIso (F.map₂CochainComplex.flip.obj ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂)) p).hom.app K₁ ≫
      (shiftFunctor (CochainComplex D ℤ) p).map ((commShiftIso (F.map₂CochainComplex.obj K₁) q).hom.app K₂) ≫
        (shiftComm ((F.map₂CochainComplex.obj K₁).obj K₂) p q).inv ≫
          (↑(CommShift₂Setup.int.ε p q)).app
            ((shiftFunctor (CochainComplex D ℤ) q).obj
              ((shiftFunctor (CochainComplex D ℤ) p).obj ((F.map₂CochainComplex.obj K₁).obj K₂)))