-- 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
comm₁₂ :
  ∀ (x : Ext.{w, v, u} S.X₂ Y n₀),
    Eq (α :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) S.X₁)
        (Functor.obj (singleFunctor C 0) Y) (↑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 preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ)
                          (↑n₀ : ℤ))
                        (Triangle.obj₂
                          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C)))
                            (op hS.singleTriangle))))
                      (Functor.map
                        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ)
                          (↑n₀ : ℤ))
                        (Triangle.mor₂
                          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C)))
                            (op hS.singleTriangle))))
                      (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
                        (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C)))
                          (op hS.singleTriangle))
                        (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
                      ⋯).f).comp
              (↑homAddEquiv :
                Ext S.X₂ Y n₀ →+ ShiftedHom ((singleFunctor C 0).obj S.X₂) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ)) :
            (a : Ext S.X₂ Y n₀) → ShiftedHom ((singleFunctor C 0).obj S.X₁) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) S.X₁)
          (Functor.obj (singleFunctor C 0) Y) (↑n₀ : ℤ))
      ((AddMonoidHom.comp
              (↑homAddEquiv :
                Ext S.X₁ Y n₀ →+ ShiftedHom ((singleFunctor C 0).obj S.X₁) ((singleFunctor C 0).obj Y) (↑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} S.X₂ Y n₀))
                    (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) (AddCommGrpCat.ofHom (precomp hS.extClass Y h))
                    ⋯).f) :
            (a : Ext S.X₂ Y n₀) → ShiftedHom ((singleFunctor C 0).obj S.X₁) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) S.X₁)
          (Functor.obj (singleFunctor C 0) Y) (↑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 preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
                (Triangle.obj₂
                  (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C)))
                    (op hS.singleTriangle))))
              (Functor.map
                (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
                (Triangle.mor₂
                  (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C)))
                    (op hS.singleTriangle))))
              (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
                (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))
                (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
              ⋯).f).comp
      (↑homAddEquiv :
        Ext S.X₂ Y n₀ →+ ShiftedHom ((singleFunctor C 0).obj S.X₂) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ)) =
    AddMonoidHom.comp
      (↑homAddEquiv : Ext S.X₁ Y n₀ →+ ShiftedHom ((singleFunctor C 0).obj S.X₁) ((singleFunctor C 0).obj Y) (↑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} S.X₂ Y n₀))
            (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) ⋯).f)

Tactic:
ext