-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
inst_4 : HasDerivedCategory.{t, v, u} C
inst_5 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
F : Functor.{v, v', u, u'} C D
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
generalize_proofs :
  ∀ (pf : HasZeroObject.{v, u} C) (pf_1 : IsRightCancelAdd ℤ) (pf_2 : IsRightCancelAdd ℤ)
    (pf_3 : F.PreservesZeroMorphisms)
    (pf_4 :
      Functor.PreservesZeroMorphisms (D := CochainComplex.{v, u, 0} C ℤ)
        (HomologicalComplex.single C (ComplexShape.up ℤ) 0))
    (pf_5 :
      Functor.PreservesZeroMorphisms (C := CochainComplex.{v, u, 0} C ℤ) (D := CochainComplex.{v', u', 0} D ℤ)
        (F.mapHomologicalComplex (ComplexShape.up ℤ)))
    (h1 :
      ShortExact (C := CochainComplex.{v', u', 0} D ℤ)
        (ShortComplex.map (C := CochainComplex.{v, u, 0} C ℤ)
          (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) (F.mapHomologicalComplex (ComplexShape.up ℤ))))
    (pf_6 : HasZeroObject.{v', u'} D)
    (pf_7 :
      Functor.PreservesZeroMorphisms (D := CochainComplex.{v', u', 0} D ℤ)
        (HomologicalComplex.single D (ComplexShape.up ℤ) 0))
    (h2 :
      ShortExact (C := CochainComplex.{v', u', 0} D ℤ)
        (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))),
    Eq.{t' + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{t', v', u'} D) (Functor.obj (singleFunctor D 0) (F.obj S.X₃))
        (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
      (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj (singleFunctor C 0) S.X₃))
        (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
        (Functor.map F.mapDerivedCategory (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors C) 0)) S.X₃) ≫
          NatTrans.app (Iso.hom F.mapDerivedCategoryFactors)
              (X₃ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))) ≫
            triangleOfSESδ h1 ≫
              CategoryStruct.comp (Y :=
                Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
                    (Functor.obj Q (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
                (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors)
                    (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))))
                (CategoryStruct.comp (Y :=
                  Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
                    (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1)
                      (Functor.obj (singleFunctor C 0) S.X₁)))
                  (NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1))
                    (Functor.obj Q (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))))
                  (NatTrans.app (Iso.hom (Functor.commShiftIso F.mapDerivedCategory 1))
                      (Functor.obj (singleFunctor C 0) S.X₁) ≫
                    Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                        (Functor.map F.mapDerivedCategory
                          (NatTrans.app
                            (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) 0))
                            S.X₁)) ≫
                      Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                        (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁)))))
      (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors D) 0)) (F.obj S.X₃) ≫
        triangleOfSESδ h2 ≫
          Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
            (NatTrans.app (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors D) Q) 0))
              (F.obj S.X₁)))
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D) (Functor.obj (singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
        (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj (singleFunctor C 0) S.X₃))
      (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
      (Functor.map F.mapDerivedCategory (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors C) 0)) S.X₃) ≫
        NatTrans.app (Iso.hom F.mapDerivedCategoryFactors)
            (X₃ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))) ≫
          CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (Functor.obj Q
                (Functor.obj (C := CochainComplex.{v, u, 0} C ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
                  (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
            (triangleOfSESδ ⋯ :
              Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
                (Functor.obj Q
                  (X₃
                    (ShortComplex.map (C := CochainComplex.{v, u, 0} C ℤ)
                      (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))
                      (F.mapHomologicalComplex (ComplexShape.up ℤ)))))
                (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (Functor.obj Q
                    (X₁
                      (ShortComplex.map (C := CochainComplex.{v, u, 0} C ℤ)
                        (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))
                        (F.mapHomologicalComplex (ComplexShape.up ℤ)))))))
            (CategoryStruct.comp (Y :=
                Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
                    (Functor.obj Q (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
                (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors)
                    (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))))
                (CategoryStruct.comp (Y :=
                  Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
                    (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1)
                      (Functor.obj (singleFunctor C 0) S.X₁)))
                  (NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1))
                    (Functor.obj Q (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))))
                  (NatTrans.app (Iso.hom (Functor.commShiftIso F.mapDerivedCategory 1))
                      (Functor.obj (singleFunctor C 0) S.X₁) ≫
                    Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                        (Functor.map F.mapDerivedCategory
                          (NatTrans.app
                            (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) 0))
                            S.X₁)) ≫
                      Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                        (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁))) :
              Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
                (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (Functor.obj Q
                    (Functor.obj (C := CochainComplex.{v, u, 0} C ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
                      (X₁ (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
                (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                  (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))))
    (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors D) 0)) (F.obj S.X₃) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (Functor.obj (singleFunctor D 0) (F.obj S.X₁)))
        (triangleOfSESδ ⋯ :
          Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
            (Functor.obj Q (X₃ (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))))
            (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (Functor.obj Q (X₁ (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))))))
        (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (NatTrans.app (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors D) Q) 0))
            (F.obj S.X₁))))

Tactic:
generalize_proofs _ _ _ _ _ _ h1 _ _ h2