Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive 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
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : 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 ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₃.Rel i₃ (c₃.next i₃)
⊢ (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)).app (K₃.X i₃) ≫
      mapBifunctor.d₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π c₂ c₁₂ (i₁, i₂)) i₃ j' =
    d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive 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
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : 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 ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)).app (K₃.X i₃) ≫
      mapBifunctor.d₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π c₂ c₁₂ (i₁, i₂)) i₃ j' =
    d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
· rw [d₃_eq _ _ _ _ _ _ _ _ _ h₁]
    by_cases h₂ : ComplexShape.π c₁₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), c₃.next i₃) = j'
    · rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂,
        ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ h₂,
        Linear.comp_units_smul, smul_left_cancel_iff,
        ι_eq _ _ _ _ _ _ _ _ _ _ _ _ rfl h₂,
        NatTrans.naturality_assoc]
    · rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂, comp_zero,
        ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₂, comp_zero, smul_zero]

Goal state after:
case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive 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
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : 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 ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)).app (K₃.X i₃) ≫
      mapBifunctor.d₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π c₂ c₁₂ (i₁, i₂)) i₃ j' =
    d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'