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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
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)).shift ↑n).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            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)).shift ↑n).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            zero := ⋯ }.g)
⊢ Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.g)

Tactic:
apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)

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 : ℕ
this✝ : HasDerivedCategory 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)).shift ↑n).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            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)).shift ↑n).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            zero := ⋯ }.g)
⊢ (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)).shift ↑n).map
                  ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
              zero := ⋯ }.f).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.f)

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 : ℕ
this✝ : HasDerivedCategory 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)).shift ↑n).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            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)).shift ↑n).map
                ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
            zero := ⋯ }.g)
⊢ (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)).shift ↑n).map
                  ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₂,
              zero := ⋯ }.g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.g)