-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (ShiftedHom.comp (b := (↑n : ℤ))
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp (b := 0)
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp (b := 0)
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (Functor.map DerivedCategory.Q (Functor.map (singleFunctor C 0) g) ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (ShiftedHom.comp
      (ShiftedHom.comp
        (ShiftedHom.mk₀ 0 ⋯
          (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
            inv (Functor.map DerivedCategory.Q R.π')))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                  R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
              (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
        ⋯)
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g)) ⋯)
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y') (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y'))
            (Cocycle.toSingleMk (((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')) ⋯)
      ⋯)

Tactic:
rw [Cocycle.toSingleMk_postcomp _ _ _ _
      (by simpa [cochainComplex_d _ _ _ m n rfl rfl]) g,
    Cocycle.equivHomShift_symm_postcomp,
    ← ShiftedHom.comp_mk₀ _ 0 rfl,
    ShiftedHom.map_comp, ShiftedHom.map_mk₀,
    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ (zero_add _) (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ (zero_add _) (zero_add _) (by simp),
    ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀, ← NatTrans.naturality]

Premises used: CategoryTheory.ShiftedHom.map_comp, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, CategoryTheory.ShiftedHom.comp_mk₀, CategoryTheory.ShiftedHom.mk₀_comp_mk₀, CategoryTheory.ShiftedHom.comp_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.ShiftedHom.map_mk₀, OfNat.ofNat, CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp, rfl