-- 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
h₂ :
  HAdd.hAdd (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
      (CategoryStruct.comp (Y := (F.obj (K₁.xNext i₁)).obj (K₂.X i₂))
        (NatTrans.app (F.map (K₁.d i₁ (c₁.next i₁))) (K₂.X i₂))
        (NatTrans.app (F.map (h₁.hom (c₁.next i₁) i₁)) (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h))
      (CategoryStruct.comp (Y := (F.obj (L₁.xPrev i₁)).obj (K₂.X i₂))
        (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂))
        (NatTrans.app (F.map (L₁.d (c₁.prev i₁) i₁)) (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h)) =
    HAdd.hAdd (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j) (β :=
        (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)
        (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) +
      HAdd.hAdd (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j) (β :=
        (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
        (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
            (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
            (CategoryStruct.comp (Y := X (L₁.mapBifunctor L₂ F c) (c.prev j))
                (hom₁ h₁ f₂ F c j (c.prev j) : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) (c.prev j))
                (HomologicalComplex₂.D₁ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂) c
                    (c.prev j) j :
                  (HomologicalComplex₂.toGradedObject
                          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂)).mapObj
                      (c₁.π c₂ c) (c.prev j) ⟶
                    (HomologicalComplex₂.toGradedObject
                          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂)).mapObj
                      (c₁.π c₂ c) j) :
              X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) :
          (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
        (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
            (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
            (CategoryStruct.comp (Y := X (L₁.mapBifunctor L₂ F c) (c.prev j))
                (hom₁ h₁ f₂ F c j (c.prev j) : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) (c.prev j))
                (HomologicalComplex₂.D₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂) c
                    (c.prev j) j :
                  (HomologicalComplex₂.toGradedObject
                          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂)).mapObj
                      (c₁.π c₂ c) (c.prev j) ⟶
                    (HomologicalComplex₂.toGradedObject
                          (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) L₁) L₂)).mapObj
                      (c₁.π c₂ c) j) :
              X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) :
          (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (Hom.f (mapBifunctorMap f₁ f₂ F c) j) =
    K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫
      (HAdd.hAdd (α := X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) (β :=
          X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j)
          (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) (c.next j)) (d (K₁.mapBifunctor K₂ F c) j (c.next j))
              (hom₁ h₁ f₂ F c (c.next j) j) :
            X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j)
          (CategoryStruct.comp (Y := X (L₁.mapBifunctor L₂ F c) (c.prev j))
              (hom₁ h₁ f₂ F c j (c.prev j) : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) (c.prev j))
              (d (L₁.mapBifunctor L₂ F c) (c.prev j) j :
                X (L₁.mapBifunctor L₂ F c) (c.prev j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
            X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j) +
        Hom.f (mapBifunctorMap f₁' f₂ F c) j)

Tactic:
simp only [ι_mapBifunctorMap, h₁.comm i₁, dNext_eq_dFrom_fromNext, dFrom, fromNext,
      AddMonoidHom.mk'_apply, prevD_eq_toPrev_dTo, toPrev, dTo, Functor.map_add,
      Functor.map_comp, NatTrans.app_add, NatTrans.comp_app,
      Preadditive.add_comp, assoc, HomologicalComplex₂.total_d,
      Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, Preadditive.comp_add,
      HomologicalComplex₂.ι_D₁_assoc, Functor.mapBifunctorHomologicalComplex_obj_obj_X_X,
      HomologicalComplex₂.ι_D₂_assoc, add_left_inj]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex₂.ι_D₁_assoc, prevD_eq_toPrev_dTo, CategoryTheory.NatTrans.app_add, CategoryTheory.Functor.map_add, HomologicalComplex₂.ι_D₂_assoc, fromNext, add_left_inj, HomologicalComplex.dTo, CategoryTheory.Preadditive.add_comp, HomologicalComplex.dFrom, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X, CategoryTheory.Preadditive.comp_add, dNext_eq_dFrom_fromNext, toPrev, Homotopy.comm, AddMonoidHom.mk'_apply, CategoryTheory.Functor.map_comp, HomologicalComplex₂.total_d, CategoryTheory.NatTrans.comp_app, HomologicalComplex.ι_mapBifunctorMap, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject