-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
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
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ 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 ≫
            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.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 (φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯
              ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
      ⋯)
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
  (ShiftedHom.comp (a := (↑n : ℤ))
    (ShiftedHom.comp
      (ShiftedHom.mk₀ (↑0 : ℤ) sorry
        (Functor.map (DerivedCategory.singleFunctor C 0) g ≫
          NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
            inv (Functor.map DerivedCategory.Q R.π')))
      (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 sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry))
        DerivedCategory.Q)
      sorry)
    (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) sorry)
  (ShiftedHom.comp (a := (↑n : ℤ))
    (ShiftedHom.comp (a := 0) (b := (↑n : ℤ))
      (ShiftedHom.mk₀ 0 sorry
        ((NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
            inv (Functor.map DerivedCategory.Q R'.π')) ≫
          Functor.map DerivedCategory.Q φ.hom'))
      (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 sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry))
        DerivedCategory.Q)
      sorry)
    (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) sorry)
Tactic: rw [Cocycle.toSingleMk_precomp _ _ _ (by lia)
    (by simpa [R.cochainComplex_d _ _ _ _ rfl rfl]),
    Cocycle.equivHomShift_symm_precomp,
    ← ShiftedHom.mk₀_comp 0 rfl, ShiftedHom.map_comp,
    ← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) _ (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) _ (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),
    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]