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
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := ⋯
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.g)
⊢ (ConcreteCategory.hom
          { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
              X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
              X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
              f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
              g :=
                (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁
                  ⋯,
              zero := ⋯ }.f).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.f)

pp: case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := ⋯
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.g)
⊢ (ConcreteCategory.hom
          { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
              X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
              X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
              f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
              g :=
                (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁
                  ⋯,
              zero := ⋯ }.g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.g)

Tactic:
· ext x; apply hom_comp_singleFunctor_map_shift (C := C)

Goal state after:
case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := ⋯
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
            g :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            zero := ⋯ }.g)
⊢ (ConcreteCategory.hom
          { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₂,
              X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
              X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
              f := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).map hS.singleTriangle.mor₂,
              g :=
                (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁
                  ⋯,
              zero := ⋯ }.g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.g)