Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
pf✝⁷ : HasZeroObject C
pf✝⁶ : IsRightCancelAdd ℤ
pf✝⁵ : IsRightCancelAdd ℤ
pf✝⁴ : F.PreservesZeroMorphisms
pf✝³ : (HomologicalComplex.single C (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
pf✝² : (F.mapHomologicalComplex (ComplexShape.up ℤ)).PreservesZeroMorphisms
h1 :
  ((S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)).map
      (F.mapHomologicalComplex (ComplexShape.up ℤ))).ShortExact
pf✝¹ : HasZeroObject D
pf✝ : (HomologicalComplex.single D (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
h2 : ((S.map F).map (HomologicalComplex.single D (ComplexShape.up ℤ) 0)).ShortExact
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃ ≫
      F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₃) ≫
        triangleOfSESδ h1 ≫
          (shiftFunctor (DerivedCategory D) 1).map
              (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app ((singleFunctor C 0).obj S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).hom.app ((singleFunctor C 0).obj S.X₁) ≫
                (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategory.map (𝟙 ((singleFunctor C 0).obj S.X₁))) ≫
                  (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    𝟙 (((singleFunctors D).functor 0).obj (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫ (shiftFunctor (DerivedCategory D) 1).map (𝟙 ((singleFunctor D 0).obj (F.obj S.X₁)))

Tactic:
Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
pf✝⁷ : HasZeroObject C
pf✝⁶ : IsRightCancelAdd ℤ
pf✝⁵ : IsRightCancelAdd ℤ
pf✝⁴ : F.PreservesZeroMorphisms
pf✝³ : (HomologicalComplex.single C (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
pf✝² : (F.mapHomologicalComplex (ComplexShape.up ℤ)).PreservesZeroMorphisms
h1 :
  ((S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)).map
      (F.mapHomologicalComplex (ComplexShape.up ℤ))).ShortExact
pf✝¹ : HasZeroObject D
pf✝ : (HomologicalComplex.single D (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
h2 : ((S.map F).map (HomologicalComplex.single D (ComplexShape.up ℤ) 0)).ShortExact
⊢ Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app S.X₃) ≫
      triangleOfSESδ h1 ≫
        (shiftFunctor (DerivedCategory D) 1).map
            (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)) ≫
          (Functor.commShiftIso F.mapDerivedCategory 1).inv.app ((singleFunctor C 0).obj S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).hom.app ((singleFunctor C 0).obj S.X₁) ≫
              (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategory.map (𝟙 ((singleFunctor C 0).obj S.X₁))) ≫
                (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    𝟙 (((singleFunctors D).functor 0).obj (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫ (shiftFunctor (DerivedCategory D) 1).map (𝟙 ((singleFunctor D 0).obj (F.obj S.X₁)))