-- Mathlib/Algebra/Homology/BifunctorShift.lean
lemma mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso :
    mapBifunctorShift₁Iso K₁ (K₂⟦y⟧) F x ≪≫
      (CategoryTheory.shiftFunctor _ x).mapIso (mapBifunctorShift₂Iso K₁ K₂ F y) =
      (x * y).negOnePow • (mapBifunctorShift₂Iso (K₁⟦x⟧) K₂ F y ≪≫
        (CategoryTheory.shiftFunctor _ y).mapIso (mapBifunctorShift₁Iso K₁ K₂ F x) ≪≫
          (shiftFunctorComm (CochainComplex D ℤ) x y).app _)

Proof state:
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{u_5, u_1} C₁
inst✝⁷ : Category.{u_6, u_2} C₂
inst✝⁶ : Category.{u_4, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ HomologicalComplex₂.total.map
        (((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
                x).hom ≫
            (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
          (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
            (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂))
        (ComplexShape.up ℤ) ≫
      (((HomologicalComplex₂.shiftFunctor₁ D x).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                  K₂)).totalShift₂Iso
            y).hom ≫
        (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) y).map
            ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₁Iso
                x).hom ≫
          (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app
            ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).total
              (ComplexShape.up ℤ)) =
    HomologicalComplex₂.total.map
        ((((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
              y).hom ≫
          (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom)
        (ComplexShape.up ℤ) ≫
      (((HomologicalComplex₂.shiftFunctor₁ D x).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                  K₂)).totalShift₂Iso
            y).hom ≫
        (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
            ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₁Iso
                x).hom ≫
          (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app (K₁.mapBifunctor K₂ F)

Tactic:
congr 2

Result:
case w.e_a.e_φ
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{u_5, u_1} C₁
inst✝⁷ : Category.{u_6, u_2} C₂
inst✝⁶ : Category.{u_4, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x).hom ≫
        (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
      (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂) =
    (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
          y).hom ≫
      (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom

Proof state:
case w.e_a.e_φ.h.h
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{u_5, u_1} C₁
inst✝⁷ : Category.{u_6, u_2} C₂
inst✝⁶ : Category.{u_4, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
a b : ℤ
⊢ ((((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
                    x).hom ≫
                (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
              (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).f
          a).f
      b =
    (((((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
                  y).hom ≫
              (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom).f
          a).f
      b

Tactic:
dsimp [HomologicalComplex₂.shiftFunctor₁₂CommIso]

Result:
case w.e_a.e_φ.h.h
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{u_5, u_1} C₁
inst✝⁷ : Category.{u_6, u_2} C₂
inst✝⁶ : Category.{u_4, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
a b : ℤ
⊢ (𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y)))) ≫
      𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) =
    𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y)))

Proof state:
case w.e_a.e_φ
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{u_5, u_1} C₁
inst✝⁷ : Category.{u_6, u_2} C₂
inst✝⁶ : Category.{u_4, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x).hom ≫
        (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
      (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂) =
    (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
          y).hom ≫
      (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom

Tactic:
ext a b

Result:
case w.e_a.e_φ.h.h
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{u_5, u_1} C₁
inst✝⁷ : Category.{u_6, u_2} C₂
inst✝⁶ : Category.{u_4, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
x y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
a b : ℤ
⊢ ((((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
                    x).hom ≫
                (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫
              (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).f
          a).f
      b =
    (((((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F
                  y).hom ≫
              (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom).f
          a).f
      b