-- 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
inst_9 : L₁.HasMapBifunctor K₂ F
n p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n
⊢ Eq (α :=
    (F.obj
            ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                  K₁).X
              p)).obj
        (K₂.X q) ⟶
      X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)) n)
    (CategoryStruct.comp (Y :=
        X
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                K₁).mapBifunctor
            K₂ F (ComplexShape.up ℤ))
          n)
        ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                K₁).ιMapBifunctor
            K₂ F (ComplexShape.up ℤ) p q n h :
          (F.obj
                  ((Functor.obj
                        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁).X
                    p)).obj
              (K₂.X q) ⟶
            X
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).mapBifunctor
                K₂ F (ComplexShape.up ℤ))
              n)
        (Hom.f
            (CategoryStruct.comp (Y :=
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    L₁).mapBifunctor
                K₂ F (ComplexShape.up ℤ))
              (mapBifunctorMap
                  (CategoryTheory.Functor.map
                    (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) f₁)
                  (𝟙 K₂) F (ComplexShape.up ℤ) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                  ((Functor.obj
                        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                        K₁).mapBifunctor
                    K₂ F (ComplexShape.up ℤ))
                  ((Functor.obj
                        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                        L₁).mapBifunctor
                    K₂ F (ComplexShape.up ℤ)))
              (Iso.hom (L₁.mapBifunctorShift₁Iso K₂ F x) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) L₁).mapBifunctor K₂
                    F)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                    (L₁.mapBifunctor K₂ F))))
            n :
          X
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).mapBifunctor
                K₂ F (ComplexShape.up ℤ))
              n ⟶
            X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F))
              n) :
      (F.obj
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).X
                p)).obj
          (K₂.X q) ⟶
        X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)) n)
    (CategoryStruct.comp (Y :=
        X
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                K₁).mapBifunctor
            K₂ F (ComplexShape.up ℤ))
          n)
        ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                K₁).ιMapBifunctor
            K₂ F (ComplexShape.up ℤ) p q n h :
          (F.obj
                  ((Functor.obj
                        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x) K₁).X
                    p)).obj
              (K₂.X q) ⟶
            X
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).mapBifunctor
                K₂ F (ComplexShape.up ℤ))
              n)
        (Hom.f
            (CategoryStruct.comp (Y :=
              Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (K₁.mapBifunctor K₂ F))
              (Iso.hom (K₁.mapBifunctorShift₁Iso K₂ F x) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) x) K₁).mapBifunctor K₂
                    F)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                    (K₁.mapBifunctor K₂ F)))
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                  (mapBifunctorMap f₁ (𝟙 K₂) F (ComplexShape.up ℤ)) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                    (K₁.mapBifunctor K₂ F))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x)
                    (HomologicalComplex.mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)))))
            n :
          X
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).mapBifunctor
                K₂ F (ComplexShape.up ℤ))
              n ⟶
            X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F))
              n) :
      (F.obj
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C₁ (ComplexShape.up ℤ)) x)
                    K₁).X
                p)).obj
          (K₂.X q) ⟶
        X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) x) (L₁.mapBifunctor K₂ F)) n)

Tactic:
simp [ι_mapBifunctorShift₁Iso_hom_f _ _ _ _ _ _ _ _ (p + x) (n + x) rfl rfl,
    ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ _ _ _ _ _ _ (p + x) (n + x) rfl rfl]

Premises used: HAdd.hAdd, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, rfl, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f