-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : Category.{v_6, u_4} C₂₃
inst_6 : HasZeroMorphisms.{v_1, u_1} C₁
inst_7 : HasZeroMorphisms.{v_2, u_2} C₂
inst_8 : HasZeroMorphisms.{v_3, u_5} C₃
inst_9 : Preadditive.{v_5, u_3} C₁₂
inst_10 : Preadditive.{v_6, u_4} C₂₃
inst_11 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
F : C₁ ⥤ CategoryTheory.Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ CategoryTheory.Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
inst_12 : F₁₂.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_14 : G.Additive
inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst_16 : G₂₃.PreservesZeroMorphisms
inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_18 : F.PreservesZeroMorphisms
inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst_20 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst_21 : TotalComplexShape c₁ c₂ c₁₂
inst_22 : TotalComplexShape c₁₂ c₃ c₄
inst_23 : TotalComplexShape c₂ c₃ c₂₃
inst_24 : TotalComplexShape c₁ c₂₃ c₄
inst_25 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_26 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_27 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_28 : DecidableEq ι₁₂
inst_29 : DecidableEq ι₂₃
inst_30 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
inst_31 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst_32 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst_33 : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
h : c₄.Rel j j'
⊢ Eq (α :=
    X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶ X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j)
        (Iso.hom (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j) :
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶
            X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j)
        (d (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j j' :
          X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j ⟶
            X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j') :
      X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (d (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j j' ≫
        Iso.hom (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j') :
      X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')

Tactic:
simp only [mapBifunctor₁₂.d_eq, mapBifunctor₂₃.d_eq _ _ _ _ _ c₁₂,
      Preadditive.add_comp, Preadditive.comp_add,
      mapBifunctorAssociatorX_hom_D₁, mapBifunctorAssociatorX_hom_D₂,
      mapBifunctorAssociatorX_hom_D₃]

Premises used: HomologicalComplex.mapBifunctor₁₂.d_eq, HomologicalComplex.mapBifunctorAssociatorX_hom_D₂, CategoryTheory.Preadditive.add_comp, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁, CategoryTheory.Preadditive.comp_add, HomologicalComplex.mapBifunctor₂₃.d_eq, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃