-- 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
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
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))
      (ShiftedHom.comp (b := 0)
        (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) ≫
            Functor.map (DerivedCategory.singleFunctor C 0) g))
        ⋯)
      ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
      (ShiftedHom.comp (b := 0)
        (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 ⋯
          (Functor.map DerivedCategory.Q φ.hom' ≫
            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.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.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) ≫ φ.hom'.f (↑n : ℤ)) ⋯ (↑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_postcomp _ (zero_add _) _ (by lia)
      (by simp [R.cochainComplex_d _ _ _ _ rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_postcomp,
    ← ShiftedHom.comp_mk₀ _ 0 rfl, ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]

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