-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
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₂
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)))
⊢ 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₂))

Tactic:
simp only [SmallShiftedHom.equiv_mk, ShiftedHom.map]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_mk, CategoryTheory.ShiftedHom.map