-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
x : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
simp :
  Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ)
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) X))
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)) (↑n : ℤ))
    (ShiftedHom.comp
      (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
              (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
          x)
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 ⋯ (inv (Functor.map DerivedCategory.Q R.ι'))) ⋯)
    (ShiftedHom.comp
      (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
              (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
          x)
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 ⋯
        (inv (Functor.map DerivedCategory.Q R.ι') ≫ 𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y)))
      ⋯)
⊢ Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ)
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) X))
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)) (↑n : ℤ))
    ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
          (a :
              SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ((singleFunctor C 0).obj X)
                ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
            ShiftedHom (DerivedCategory.Q.obj ((singleFunctor C 0).obj X))
              (DerivedCategory.Q.obj ((singleFunctor C 0).obj Y)) (↑n : ℤ))
        (SmallShiftedHom.comp (W := HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
          (CohomologyClass.mk x).toSmallShiftedHom
          (SmallShiftedHom.mk₀Inv (W := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) 0 ⋯ R.ι' ⋯) ⋯) :
      ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ)
        (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) X))
        (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)) (↑n : ℤ))
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
                  (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
              x)
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯
            (inv (Functor.map DerivedCategory.Q R.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
          ⋯)
        ⋯ :
      ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
simp only [SmallShiftedHom.equiv_comp, CohomologyClass.equiv_toSmallShiftedHom_mk,
    SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv, Functor.comp_obj,
    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Iso.refl_inv,
    ShiftedHom.mk₀_id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Localization.SmallShiftedHom.equiv_comp, DerivedCategory.singleFunctorIsoCompQ, CategoryTheory.ShiftedHom.mk₀_id_comp, CategoryTheory.asIso_inv, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Localization.isoOfHom, CategoryTheory.Iso.refl_inv, CategoryTheory.NatTrans.id_app, CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv, CategoryTheory.Iso.refl_hom