-- 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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
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.comp (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g))
        (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)
            (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (inv (Functor.map DerivedCategory.Q R.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
        ⋯)
      ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X'))
      (ShiftedHom.comp (b := (↑n : ℤ))
        (ShiftedHom.map (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) g)) DerivedCategory.Q)
        (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)
              (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯
            (inv (Functor.map DerivedCategory.Q R.ι') ≫
              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.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))
        (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)
              (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯
            (inv (Functor.map DerivedCategory.Q R.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
          ⋯)
        ⋯)
      ⋯)
    (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)
            (Cocycle.fromSingleMk (g ≫ f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (inv (Functor.map DerivedCategory.Q R.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
        ⋯)
      ⋯)

Tactic:
rw [Cocycle.fromSingleMk_precomp g _ (zero_add _) _ (by lia) (by
      simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_precomp, ← ShiftedHom.mk₀_comp 0 rfl,
    ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) (add_zero (n : ℤ)) (by simp)]

Premises used: CategoryTheory.ShiftedHom.map_comp, CategoryTheory.ShiftedHom.mk₀_comp, zero_add, Nat.cast, CategoryTheory.ShiftedHom.comp_assoc, CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, add_zero, OfNat.ofNat, rfl