-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
pos :
  ∀ (h₄ : c₂.Rel i₂ (c₂.next i₂)),
    Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
      (CategoryStruct.comp (Y :=
          (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
          (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
              (c.next j) :
            X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
              (HomologicalComplex₂.toGradedObject
                    (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
                (c₁.π c₂ c) (c.next j))
          (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
        (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
      (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
neg :
  ∀ (h₄ : ¬c₂.Rel i₂ (c₂.next i₂)),
    Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
      (CategoryStruct.comp (Y :=
          (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
          (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
              (c.next j) :
            X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
              (HomologicalComplex₂.toGradedObject
                    (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
                (c₁.π c₂ c) (c.next j))
          (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
        (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
      (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)

Tactic:
by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)

Premises used: ComplexShape.next, ComplexShape.Rel