-- 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
dsimp :
  CategoryStruct.comp (Y :=
      X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
      (K₁.ιMapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F n₁ n₂ n
          h :
        (F.obj (K₁.X n₁)).obj
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂).X n₂) ⟶
          X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
      (CategoryStruct.comp (Y :=
          X
            (HomologicalComplex₂.total
              (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁)
                  K₂))
              (ComplexShape.up ℤ))
            n)
          (Hom.f
              (HomologicalComplex₂.total.map (Iso.hom (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y))
                (ComplexShape.up ℤ))
              n :
            X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
                n ⟶
              X
                (HomologicalComplex₂.total
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  (ComplexShape.up ℤ))
                n)
          (Hom.f
              (Iso.hom
                (HomologicalComplex₂.totalShift₂Iso
                  (Functor.obj
                    (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂)
                  y))
              n :
            X
                (HomologicalComplex₂.total
                  (Functor.obj (HomologicalComplex₂.shiftFunctor₂ D y)
                    (Functor.obj
                      (Functor.obj (F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)) K₁) K₂))
                  (ComplexShape.up ℤ))
                n ⟶
              X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))
                n) :
        X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n ⟶
          X (K₁.mapBifunctor K₂ F) (n + y)) =
    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) ⋯))
⊢ CategoryStruct.comp (Y :=
      X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
      (K₁.ιMapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F n₁ n₂ n
          h :
        (F.obj (K₁.X n₁)).obj
            ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂).X n₂) ⟶
          X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n)
      (Hom.f (Iso.hom (K₁.mapBifunctorShift₂Iso K₂ F y)) n :
        X (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F) n ⟶
          X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F)) n) =
    HSMul.hSMul (β :=
      (F.obj (K₁.X n₁)).obj ((Functor.obj (shiftFunctor C₂ y) K₂).X n₂) ⟶
        X (Functor.obj (shiftFunctor D y) (K₁.mapBifunctor K₂ F)) n)
      (n₁ * y).negOnePow
      ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ Iso.inv (shiftFunctorObjXIso (K₁.mapBifunctor K₂ F) y n m hm))

Tactic:
dsimp [mapBifunctorShift₂Iso]

Premises used: CochainComplex.mapBifunctorShift₂Iso