-- 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)
x : Ext.{w, v, u} S.X₁ Y n₀
comm₂₃ :
  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) (X :=
              Functor.obj
                (Functor.shift
                  (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                    forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                      fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                      LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                        (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                        (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                      (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                  (M := ℤ) (↑n₀ : ℤ))
                (op (Functor.obj (singleFunctor C 0) S.X₁)))
              (Y :=
              Functor.obj
                (Functor.shift
                  (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                    forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                      fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                      LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                        (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                        (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                      (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                  (M := ℤ) (↑n₁ : ℤ))
                (op (Functor.obj (singleFunctor C 0) S.X₃)))
              (Functor.homologySequenceδ
                  (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                    forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                      fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                      LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                        (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                        (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                      (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                  (Triangle.mk (X := op (Functor.obj (singleFunctor C 0) S.X₃))
                    (Quiver.Hom.op (Functor.map (singleFunctor C 0) S.g))
                    (Quiver.Hom.op (Functor.map (singleFunctor C 0) S.f))
                    (CategoryStruct.comp (Y :=
                      Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                        (op
                          (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) 1)
                            (Functor.obj (singleFunctor C 0) S.X₁))))
                      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence (DerivedCategory C) 1)))
                          (op (Functor.obj (singleFunctor C 0) S.X₁)) :
                        Quiver.Hom (V := (DerivedCategory C)ᵒᵖ)
                          (Functor.obj (𝟭 (DerivedCategory C)ᵒᵖ) (op (Functor.obj (singleFunctor C 0) S.X₁)))
                          (Functor.obj
                            (Functor.op (shiftFunctor (DerivedCategory C) (A := ℤ) 1) ⋙
                              shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                            (op (Functor.obj (singleFunctor C 0) S.X₁))))
                      (Functor.map (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1) (Quiver.Hom.op hS.singleδ) :
                        Quiver.Hom (V := (DerivedCategory C)ᵒᵖ)
                          (Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                            (op
                              (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) 1)
                                (Functor.obj (singleFunctor C 0) S.X₁))))
                          (Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                            (op (Functor.obj (singleFunctor C 0) S.X₃))))))
                  (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯ :
                Functor.obj
                    (Functor.shift
                      (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                        forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                          fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                          LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                            (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                            (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                      (M := ℤ) (↑n₀ : ℤ))
                    (Triangle.obj₃
                      (Triangle.mk (X := op (Functor.obj (singleFunctor C 0) S.X₃))
                        (Quiver.Hom.op (Functor.map (singleFunctor C 0) S.g))
                        (Quiver.Hom.op (Functor.map (singleFunctor C 0) S.f))
                        (CategoryStruct.comp (Y :=
                          Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                            (op
                              (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) 1)
                                (Functor.obj (singleFunctor C 0) S.X₁))))
                          (NatTrans.app
                              (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence (DerivedCategory C) 1)))
                              (op (Functor.obj (singleFunctor C 0) S.X₁)) :
                            Quiver.Hom (V := (DerivedCategory C)ᵒᵖ)
                              (Functor.obj (𝟭 (DerivedCategory C)ᵒᵖ) (op (Functor.obj (singleFunctor C 0) S.X₁)))
                              (Functor.obj
                                (Functor.op (shiftFunctor (DerivedCategory C) (A := ℤ) 1) ⋙
                                  shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                                (op (Functor.obj (singleFunctor C 0) S.X₁))))
                          (Functor.map (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1) (Quiver.Hom.op hS.singleδ) :
                            Quiver.Hom (V := (DerivedCategory C)ᵒᵖ)
                              (Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                                (op
                                  (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) 1)
                                    (Functor.obj (singleFunctor C 0) S.X₁))))
                              (Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                                (op (Functor.obj (singleFunctor C 0) S.X₃))))))) ⟶
                  Functor.obj
                    (Functor.shift
                      (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                        forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                          fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                          LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                            (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                            (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                      (M := ℤ) (↑n₁ : ℤ))
                    (Triangle.obj₁
                      (Triangle.mk (X := op (Functor.obj (singleFunctor C 0) S.X₃))
                        (Quiver.Hom.op (Functor.map (singleFunctor C 0) S.g))
                        (Quiver.Hom.op (Functor.map (singleFunctor C 0) S.f))
                        (CategoryStruct.comp (Y :=
                          Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                            (op
                              (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) 1)
                                (Functor.obj (singleFunctor C 0) S.X₁))))
                          (NatTrans.app
                              (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence (DerivedCategory C) 1)))
                              (op (Functor.obj (singleFunctor C 0) S.X₁)) :
                            Quiver.Hom (V := (DerivedCategory C)ᵒᵖ)
                              (Functor.obj (𝟭 (DerivedCategory C)ᵒᵖ) (op (Functor.obj (singleFunctor C 0) S.X₁)))
                              (Functor.obj
                                (Functor.op (shiftFunctor (DerivedCategory C) (A := ℤ) 1) ⋙
                                  shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                                (op (Functor.obj (singleFunctor C 0) S.X₁))))
                          (Functor.map (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1) (Quiver.Hom.op hS.singleδ) :
                            Quiver.Hom (V := (DerivedCategory C)ᵒᵖ)
                              (Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                                (op
                                  (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) 1)
                                    (Functor.obj (singleFunctor C 0) S.X₁))))
                              (Functor.obj (shiftFunctor (DerivedCategory C)ᵒᵖ (A := ℤ) 1)
                                (op (Functor.obj (singleFunctor C 0) S.X₃)))))))) :
            (↑(Functor.obj
                    (Functor.shift
                      (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                        forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                          fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                          LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                            (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                            (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                      (M := ℤ) (↑n₀ : ℤ))
                    (op (Functor.obj (singleFunctor C 0) S.X₁))) :
                Type (max u v)) →+
              (↑(Functor.obj
                    (Functor.shift
                      (preadditiveYonedaObj (Functor.obj (singleFunctor C 0) Y) ⋙
                        forget₂ (ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) (FC :=
                          fun (x1 x2 : ModuleCat (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))) ↦
                          LinearMap (R := End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y))
                            (RingHom.id (End (C := DerivedCategory C) (Functor.obj (singleFunctor C 0) Y)))
                            (↑x1 : Type (max u v)) (↑x2 : Type (max u v)))
                          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommGrpCat.carrier))
                      (M := ℤ) (↑n₁ : ℤ))
                    (op (Functor.obj (singleFunctor C 0) S.X₃))) :
                Type (max u v))) :
          (a : ShiftedHom ((singleFunctor C 0).obj S.X₁) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ)) →
            ShiftedHom ((singleFunctor C 0).obj S.X₃) ((singleFunctor C 0).obj Y) (↑n₁ : ℤ))
        x.hom :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) S.X₃)
        (Functor.obj (singleFunctor C 0) Y) (↑n₁ : ℤ))
    ((comp hS.extClass x h).hom :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) S.X₃)
        (Functor.obj (singleFunctor C 0) 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₁ : ℤ) ⋯)
                    ⋯).g).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)) ⋯).g) :
          (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₁ : ℤ))

Tactic:
dsimp