-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Eq (α := ShiftedHom (C := DerivedCategory C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L) n)
    ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
        (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
          ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
      ((fun (y : Cocycle K L n) ↦
          (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
              ((AddEquiv.symm Cocycle.equivHomShift :
                  (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
                y) :
            SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
        y₁))
    ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
        (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
          ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
      ((fun (y : Cocycle K L n) ↦
          (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
              ((AddEquiv.symm Cocycle.equivHomShift :
                  (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
                y) :
            SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
        y₂))
have simp : Eq (α := ShiftedHom (C := DerivedCategory C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L) n)
  (CategoryStruct.comp (Y :=
      Functor.obj DerivedCategory.Q (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
      (CategoryTheory.Functor.map DerivedCategory.Q
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
          y₁))
      (NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q n)) L) :
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q K)
      (Functor.obj (CategoryTheory.shiftFunctor (DerivedCategory C) n) (Functor.obj DerivedCategory.Q L)))
  (CategoryStruct.comp (Y :=
      Functor.obj DerivedCategory.Q (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
      (CategoryTheory.Functor.map DerivedCategory.Q
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
          y₂))
      (NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q n)) L) :
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q K)
      (Functor.obj (CategoryTheory.shiftFunctor (DerivedCategory C) n) (Functor.obj DerivedCategory.Q L)))
Tactic: simp only [SmallShiftedHom.equiv_mk, ShiftedHom.map]