-- 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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this_1 : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this_2 : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this_3 : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (C := K₁.mapBifunctor K₂ F c) (D := L₁.mapBifunctor L₂ F c) (mapBifunctorMap f₁ f₂ F c)
  (mapBifunctorMap f₁ f₂' F c) :=
  Homotopy.trans (f :=
    CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
      (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c) (K₂.mapBifunctor K₁ F.flip c))
      (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
          (mapBifunctorMap f₂ f₁ F.flip c :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
              (L₂.mapBifunctor L₁ F.flip c))
          (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
              (L₁.mapBifunctor L₂ F c)) :
        Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
          (L₁.mapBifunctor L₂ F c)))
    (Homotopy.ofEq ⋯ :
      Homotopy (C := K₁.mapBifunctor K₂ F c) (D := L₁.mapBifunctor L₂ F c) (mapBifunctorMap f₁ f₂ F c)
        (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
          (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c)
              (K₂.mapBifunctor K₁ F.flip c))
          (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
              (mapBifunctorMap f₂ f₁ F.flip c :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                  (L₂.mapBifunctor L₁ F.flip c))
              (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
                  (L₁.mapBifunctor L₂ F c)) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
              (L₁.mapBifunctor L₂ F c))))
    (Homotopy.trans (f :=
        CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
          (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c)
              (K₂.mapBifunctor K₁ F.flip c))
          (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
              (mapBifunctorMap f₂' f₁ F.flip c :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                  (L₂.mapBifunctor L₁ F.flip c))
              (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
                  (L₁.mapBifunctor L₂ F c)) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
              (L₁.mapBifunctor L₂ F c)))
        (Homotopy.compLeft
            (Homotopy.compRight (mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c) (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c)))
            (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c)) :
          Homotopy (C := K₁.mapBifunctor K₂ F c) (D := L₁.mapBifunctor L₂ F c)
            (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
              (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c)
                  (K₂.mapBifunctor K₁ F.flip c))
              (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
                  (mapBifunctorMap f₂ f₁ F.flip c :
                    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                      (L₂.mapBifunctor L₁ F.flip c))
                  (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
                    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
                      (L₁.mapBifunctor L₂ F c)) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                  (L₁.mapBifunctor L₂ F c)))
            (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
              (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c)
                  (K₂.mapBifunctor K₁ F.flip c))
              (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
                  (mapBifunctorMap f₂' f₁ F.flip c :
                    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                      (L₂.mapBifunctor L₁ F.flip c))
                  (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
                    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
                      (L₁.mapBifunctor L₂ F c)) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                  (L₁.mapBifunctor L₂ F c))))
        (Homotopy.ofEq ⋯ :
          Homotopy (C := K₁.mapBifunctor K₂ F c) (D := L₁.mapBifunctor L₂ F c)
            (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
              (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c)
                  (K₂.mapBifunctor K₁ F.flip c))
              (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
                  (mapBifunctorMap f₂' f₁ F.flip c :
                    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                      (L₂.mapBifunctor L₁ F.flip c))
                  (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
                    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
                      (L₁.mapBifunctor L₂ F c)) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                  (L₁.mapBifunctor L₂ F c)))
            (mapBifunctorMap f₁ f₂' F c)) :
      Homotopy (C := K₁.mapBifunctor K₂ F c) (D := L₁.mapBifunctor L₂ F c)
        (CategoryStruct.comp (Y := K₂.mapBifunctor K₁ F.flip c)
          (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c)
              (K₂.mapBifunctor K₁ F.flip c))
          (CategoryStruct.comp (Y := L₂.mapBifunctor L₁ F.flip c)
              (mapBifunctorMap f₂ f₁ F.flip c :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
                  (L₂.mapBifunctor L₁ F.flip c))
              (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (L₂.mapBifunctor L₁ F.flip c)
                  (L₁.mapBifunctor L₂ F c)) :
            Quiver.Hom (V := HomologicalComplex.{v_3, u_3, u_6} D c) (K₂.mapBifunctor K₁ F.flip c)
              (L₁.mapBifunctor L₂ F c)))
        (mapBifunctorMap f₁ f₂' F c))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
h :
  HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₂ c₂ c (i₁, c₂.prev i₂))
      ((F.map (f₁.f i₁)).app (K₂.X i₂) ≫
        CategoryStruct.comp (Y := (F.obj (L₁.X i₁)).obj (L₂.X (c₂.prev i₂)))
          ((F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂))) (L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂) j')) =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.σ c₂ c i₁ i₂)
      (HSMul.hSMul (β := (F.flip.obj (K₂.X i₂)).obj (K₁.X i₁) ⟶ X (L₂.mapBifunctor L₁ F.flip c) j')
          (c₂.ε₁ c₁ c (c₂.prev i₂, i₁))
          (NatTrans.app (F.flip.map (h₂.hom i₂ (c₂.prev i₂))) (K₁.X i₁) ≫
            (F.flip.obj (L₂.X (c₂.prev i₂))).map (f₁.f i₁) ≫ L₂.ιMapBifunctorOrZero L₁ F.flip c (c₂.prev i₂) i₁ j') ≫
        Hom.f (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c)) j')
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₂ f₁ h₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫
      (0 +
        HAdd.hAdd (α := X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j')
          (CategoryStruct.comp (Y := X (K₂.mapBifunctor K₁ F.flip c) j)
            (Hom.f (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c)) j :
              X (K₁.mapBifunctor K₂ F c) j ⟶ X (K₂.mapBifunctor K₁ F.flip c) j)
            (CategoryStruct.comp (Y := X (L₂.mapBifunctor L₁ F.flip c) j')
                (hom₁ h₂ f₁ F.flip c j j' : X (K₂.mapBifunctor K₁ F.flip c) j ⟶ X (L₂.mapBifunctor L₁ F.flip c) j')
                (Hom.f (Iso.hom (L₁.mapBifunctorFlipIso L₂ F c)) j' :
                  X (L₂.mapBifunctor L₁ F.flip c) j' ⟶ X (L₁.mapBifunctor L₂ F c) j') :
              X (K₂.mapBifunctor K₁ F.flip c) j ⟶ X (L₁.mapBifunctor L₂ F c) j'))
          0)

Tactic:
rw [add_zero, zero_add, ι_mapBifunctorFlipIso_inv_assoc, Linear.units_smul_comp,
      ιMapBifunctor_hom₁_assoc h₂ f₁ F.flip c _ i₂ i₁ j j'
        (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]) rfl,
      ιMapBifunctor_hom₂ f₁ h₂ F c i₁ _ i₂ j j' hj rfl]

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Linear.units_smul_comp, HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc, zero_add, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, add_zero, rfl