Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ L₂ : CochainComplex C₂ ℤ
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Hom.isoOfComponents
              (fun x ↦
                Iso.refl
                  (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                        i).X
                    x))
              ⋯).hom ≫
          ((HomologicalComplex₂.shiftFunctor₂ D y).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).d
            i j =
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).d
            i j ≫
          (Hom.isoOfComponents
              (fun x ↦
                Iso.refl
                  (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                        j).X
                    x))
              ⋯).hom

Tactic:
intros

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ L₂ : CochainComplex C₂ ℤ
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
i✝ j✝ : ℤ
a✝ : (ComplexShape.up ℤ).Rel i✝ j✝
⊢ (Hom.isoOfComponents
          (fun x ↦
            Iso.refl
              (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                        ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                    i✝).X
                x))
          ⋯).hom ≫
      ((HomologicalComplex₂.shiftFunctor₂ D y).obj
            (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).d
        i✝ j✝ =
    (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).d
        i✝ j✝ ≫
      (Hom.isoOfComponents
          (fun x ↦
            Iso.refl
              (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                        ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                    j✝).X
                x))
          ⋯).hom