-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact (M :=
    (↑(ShortComplex.mk (X₁ :=
            Functor.obj (C := DerivedCategory C)
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.obj₂ hS.singleTriangle))
            (Functor.map
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.mor₂ hS.singleTriangle))
            (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
              hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
            ⋯).X₁ :
      Type (max u v)))
    (N :=
    (↑(ShortComplex.mk (X₁ :=
            Functor.obj (C := DerivedCategory C)
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.obj₂ hS.singleTriangle))
            (Functor.map
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.mor₂ hS.singleTriangle))
            (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
              hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
            ⋯).X₂ :
      Type (max u v)))
    (P :=
    (↑(ShortComplex.mk (X₁ :=
            Functor.obj (C := DerivedCategory C)
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.obj₂ hS.singleTriangle))
            (Functor.map
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.mor₂ hS.singleTriangle))
            (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
              hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
            ⋯).X₃ :
      Type (max u v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CC := AddCommGrpCat.carrier)
          (ShortComplex.mk (X₁ :=
              Functor.obj (C := DerivedCategory C)
                (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                  (↑n₀ : ℤ))
                (Triangle.obj₂ hS.singleTriangle))
              (Functor.map
                (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                  (↑n₀ : ℤ))
                (Triangle.mor₂ hS.singleTriangle))
              (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
                hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
              ⋯).f) :
      (a :
          (↑{
                  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 := ⋯ }.X₁ :
            Type (max u v))) →
        (↑{
                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 := ⋯ }.X₂ :
          Type (max u v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CC := AddCommGrpCat.carrier)
          (ShortComplex.mk (X₁ :=
              Functor.obj (C := DerivedCategory C)
                (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                  (↑n₀ : ℤ))
                (Triangle.obj₂ hS.singleTriangle))
              (Functor.map
                (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                  (↑n₀ : ℤ))
                (Triangle.mor₂ hS.singleTriangle))
              (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
                hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
              ⋯).g) :
      (a :
          (↑{
                  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 := ⋯ }.X₂ :
            Type (max u v))) →
        (↑{
                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 := ⋯ }.X₃ :
          Type (max u v)))
comm₂₃ :
  ∀ (x : Ext.{w, v, u} X S.X₃ n₀),
    Eq (α :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) S.X₁) (↑n₁ : ℤ))
      (((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                  (CC := AddCommGrpCat.carrier)
                  (ShortComplex.mk (X₁ :=
                      Functor.obj (C := DerivedCategory C)
                        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M :=
                          ℤ) (↑n₀ : ℤ))
                        (Triangle.obj₂ hS.singleTriangle))
                      (Functor.map
                        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M :=
                          ℤ) (↑n₀ : ℤ))
                        (Triangle.mor₂ hS.singleTriangle))
                      (Functor.homologySequenceδ
                        (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) hS.singleTriangle
                        (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
                      ⋯).g).comp
              (↑homAddEquiv :
                Ext X S.X₃ n₀ →+ ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj S.X₃) (↑n₀ : ℤ)) :
            (a : Ext X S.X₃ n₀) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj S.X₁) (↑n₁ : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (singleFunctor C 0) S.X₁) (↑n₁ : ℤ))
      ((AddMonoidHom.comp
              (↑homAddEquiv :
                Ext X S.X₁ n₁ →+ ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj S.X₁) (↑n₁ : ℤ))
              (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier)
                (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀))
                    (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯)) (AddCommGrpCat.ofHom (postcomp hS.extClass X h))
                    ⋯).g) :
            (a : Ext X S.X₃ n₀) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj S.X₁) (↑n₁ : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (singleFunctor C 0) S.X₁) (↑n₁ : ℤ))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
          AddCommGrpCat.carrier)
          (ShortComplex.mk (X₁ :=
              Functor.obj (C := DerivedCategory C)
                (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                  (↑n₀ : ℤ))
                (Triangle.obj₂ hS.singleTriangle))
              (Functor.map
                (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                  (↑n₀ : ℤ))
                (Triangle.mor₂ hS.singleTriangle))
              (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
                hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
              ⋯).g).comp
      (↑homAddEquiv :
        Ext X S.X₃ n₀ →+ ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj S.X₃) (↑n₀ : ℤ)) =
    AddMonoidHom.comp
      (↑homAddEquiv : Ext X S.X₁ n₁ →+ ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj S.X₁) (↑n₁ : ℤ))
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
        AddCommGrpCat.carrier)
        (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀))
            (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯)) (AddCommGrpCat.ofHom (postcomp hS.extClass X h)) ⋯).g)

Tactic:
ext x