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 : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard 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))).shift ↑n).map hS.singleTriangle.mor₂,
            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))).shift ↑n).map hS.singleTriangle.mor₂,
            zero := ⋯ }.g)
x : Ext X S.X₂ n
⊢ ((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))).shift ↑n).map hS.singleTriangle.mor₂,
                zero := ⋯ }.g).comp
        ↑homAddEquiv)
      x =
    ((↑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.f).postcomp X ⋯),
              g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯), zero := ⋯ }.g))
      x

Tactic:
;

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 : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard 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))).shift ↑n).map hS.singleTriangle.mor₂,
            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))).shift ↑n).map hS.singleTriangle.mor₂,
            zero := ⋯ }.g)
x : Ext X S.X₂ n
⊢ ((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))).shift ↑n).map hS.singleTriangle.mor₂,
                zero := ⋯ }.g).comp
        ↑homAddEquiv)
      x =
    ((↑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.f).postcomp X ⋯),
              g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯), zero := ⋯ }.g))
      x