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₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  {
      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 := ⋯ }.Exact
⊢ { 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.f).precomp Y ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact

Tactic:
rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢

Goal state after:
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)
⊢ 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.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), 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.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.g)