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

Goal state before:
pp: case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        {
            X₁ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₂,
            X₂ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₃,
            X₃ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₁,
            f :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            g :=
              (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        {
            X₁ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₂,
            X₂ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₃,
            X₃ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₁,
            f :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            g :=
              (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.g)
x✝ : Ext S.X₁ Y n₀
⊢ ((ConcreteCategory.hom
            ((preadditiveYonedaObj ((singleFunctor C 0).obj Y) ⋙
                  forget₂ (ModuleCat (End ((singleFunctor C 0).obj Y))) AddCommGrpCat).homologySequenceδ
              (Triangle.mk ((singleFunctor C 0).map S.g).op ((singleFunctor C 0).map S.f).op
                ((opShiftFunctorEquivalence (DerivedCategory C) 1).counitIso.inv.app
                    (op ((singleFunctor C 0).obj S.X₁)) ≫
                  (shiftFunctor (DerivedCategory C)ᵒᵖ 1).map hS.singleδ.op))
              ↑n₀ ↑n₁ ⋯)).comp
        ↑homAddEquiv)
      x✝ =
    (hS.extClass.comp x✝ h).hom

Tactic:
;

Goal state after:
case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        {
            X₁ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₂,
            X₂ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₃,
            X₃ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₁,
            f :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            g :=
              (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        {
            X₁ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₂,
            X₂ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₃,
            X₃ :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).obj
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₁,
            f :=
              ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            g :=
              (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.g)
x✝ : Ext S.X₁ Y n₀
⊢ ((ConcreteCategory.hom
            ((preadditiveYonedaObj ((singleFunctor C 0).obj Y) ⋙
                  forget₂ (ModuleCat (End ((singleFunctor C 0).obj Y))) AddCommGrpCat).homologySequenceδ
              (Triangle.mk ((singleFunctor C 0).map S.g).op ((singleFunctor C 0).map S.f).op
                ((opShiftFunctorEquivalence (DerivedCategory C) 1).counitIso.inv.app
                    (op ((singleFunctor C 0).obj S.X₁)) ≫
                  (shiftFunctor (DerivedCategory C)ᵒᵖ 1).map hS.singleδ.op))
              ↑n₀ ↑n₁ ⋯)).comp
        ↑homAddEquiv)
      x✝ =
    (hS.extClass.comp x✝ h).hom