Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: 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✝²⁸ : Category.{v_2, u_2} C₂
inst✝²⁷ : Category.{v_3, u_5} C₃
inst✝²⁶ : Category.{v_4, u_6} C₄
inst✝²⁵ : Category.{v_5, u_3} C₁₂
inst✝²⁴ : Category.{v_6, u_4} C₂₃
inst✝²³ : HasZeroMorphisms C₁
inst✝²² : HasZeroMorphisms C₂
inst✝²¹ : HasZeroMorphisms C₃
inst✝²⁰ : Preadditive C₁₂
inst✝¹⁹ : Preadditive C₂₃
inst✝¹⁸ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹⁷ : F₁₂.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁵ : G.Additive
inst✝¹⁴ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (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✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₂₃ : ι₂₃
j : ι₄
h₂₃ : c₂.π c₃ c₂₃ (i₂, i₃) = i₂₃
h : c₁.π c₂₃ c₄ (i₁, i₂₃) = j
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃)

Tactic:
;

Goal state after:
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✝²⁸ : Category.{v_2, u_2} C₂
inst✝²⁷ : Category.{v_3, u_5} C₃
inst✝²⁶ : Category.{v_4, u_6} C₄
inst✝²⁵ : Category.{v_5, u_3} C₁₂
inst✝²⁴ : Category.{v_6, u_4} C₂₃
inst✝²³ : HasZeroMorphisms C₁
inst✝²² : HasZeroMorphisms C₂
inst✝²¹ : HasZeroMorphisms C₃
inst✝²⁰ : Preadditive C₁₂
inst✝¹⁹ : Preadditive C₂₃
inst✝¹⁸ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹⁷ : F₁₂.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁵ : G.Additive
inst✝¹⁴ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (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✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₂₃ : ι₂₃
j : ι₄
h₂₃ : c₂.π c₃ c₂₃ (i₂, i₃) = i₂₃
h : c₁.π c₂₃ c₄ (i₁, i₂₃) = j
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃)