-- Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
lemma singleFunctorsPostcompQIso_hom_hom (n : ℤ) :
    (singleFunctorsPostcompQIso C).hom.hom n = 𝟙 _

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
rfl

Result:
no goals

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ (((SingleFunctors.postcompFunctor C ℤ Qh).map (𝟙 (HomotopyCategory.singleFunctors C))).hom n).app X ≫
      𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X))) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
rw [CategoryTheory.Functor.map_id, SingleFunctors.id_hom, NatTrans.id_app]

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 ((((SingleFunctors.postcompFunctor C ℤ Qh).obj (HomotopyCategory.singleFunctors C)).functor n).obj X) ≫
      𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X))) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ (singleFunctorsPostcompQIso C).hom.hom n = 𝟙 ((singleFunctors C).functor n)

Tactic:
ext X

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ ((singleFunctorsPostcompQIso C).hom.hom n).app X = (𝟙 ((singleFunctors C).functor n)).app X

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ ((singleFunctorsPostcompQIso C).hom.hom n).app X = (𝟙 ((singleFunctors C).functor n)).app X

Tactic:
dsimp [singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso,
  quotientCompQhIso, HomologicalComplexUpToQuasiIso.quotientCompQhIso]

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ (((SingleFunctors.postcompFunctor C ℤ Qh).map (𝟙 (HomotopyCategory.singleFunctors C))).hom n).app X ≫
      𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X))) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 ((((SingleFunctors.postcompFunctor C ℤ Qh).obj (HomotopyCategory.singleFunctors C)).functor n).obj X) ≫
      𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X))) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
erw [Category.id_comp, Category.id_comp]

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)