-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
x : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
⊢ Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom.{u_1, w, v, u}
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk x)))
    (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))
        ⋯)
      ⋯)
have change : 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 sorry R.ι' sorry) sorry) :
    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 sorry (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 sorry
          (inv (Functor.map DerivedCategory.Q R.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
        sorry)
      sorry :
    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: change SmallShiftedHom.equiv _ _ ((CohomologyClass.mk x).toSmallShiftedHom.comp _ _) = _