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
F : C ⥤ D
inst✝⁶ : F.Additive
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : PreservesFiniteColimits F
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
n : ℕ
e : Ext X Y n
this :
  (mapExactFunctor F e).hom =
    (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
            F.mapDerivedCategoryFactors.symm.hom.app ((CochainComplex.singleFunctor C 0).obj X))).comp
      ((((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q) e).map
            F.mapDerivedCategory).comp
        (ShiftedHom.mk₀ 0 ⋯
          (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
            DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom))
        ⋯)
      ⋯
⊢ (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
            F.mapDerivedCategoryFactors.symm.hom.app ((CochainComplex.singleFunctor C 0).obj X))).comp
      ((((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q) e).map
            F.mapDerivedCategory).comp
        (ShiftedHom.mk₀ 0 ⋯
          (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
            DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((F.mapDerivedCategorySingleFunctor 0).inv.app X)).comp
      ((e.hom.map F.mapDerivedCategory).comp (ShiftedHom.mk₀ 0 ⋯ ((F.mapDerivedCategorySingleFunctor 0).hom.app Y)) ⋯) ⋯

Tactic:
congr 2

Goal state after:
case e_f
C : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Abelian C
D : Type u'
inst✝⁸ : Category.{v', u'} D
inst✝⁷ : Abelian D
F : C ⥤ D
inst✝⁶ : F.Additive
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : PreservesFiniteColimits F
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
n : ℕ
e : Ext X Y n
this :
  (mapExactFunctor F e).hom =
    (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
            F.mapDerivedCategoryFactors.symm.hom.app ((CochainComplex.singleFunctor C 0).obj X))).comp
      ((((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q) e).map
            F.mapDerivedCategory).comp
        (ShiftedHom.mk₀ 0 ⋯
          (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
            DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom))
        ⋯)
      ⋯
⊢ DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
      F.mapDerivedCategoryFactors.symm.hom.app ((CochainComplex.singleFunctor C 0).obj X) =
    (F.mapDerivedCategorySingleFunctor 0).inv.app X

case e_g
C : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Abelian C
D : Type u'
inst✝⁸ : Category.{v', u'} D
inst✝⁷ : Abelian D
F : C ⥤ D
inst✝⁶ : F.Additive
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : PreservesFiniteColimits F
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
n : ℕ
e : Ext X Y n
this :
  (mapExactFunctor F e).hom =
    (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
            F.mapDerivedCategoryFactors.symm.hom.app ((CochainComplex.singleFunctor C 0).obj X))).comp
      ((((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q) e).map
            F.mapDerivedCategory).comp
        (ShiftedHom.mk₀ 0 ⋯
          (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
            DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom))
        ⋯)
      ⋯
⊢ ShiftedHom.mk₀ 0 ⋯
      (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
        DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom) =
    ShiftedHom.mk₀ 0 ⋯ ((F.mapDerivedCategorySingleFunctor 0).hom.app Y)