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

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

Tactic:
erw [CategoryTheory.Functor.map_id]

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)) ≫
        𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X)))) ≫
      ((𝟙
                ((SingleFunctors.postcompFunctor C ℤ Qh).obj
                  ((CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ))))).hom
            n).app
        X =
    𝟙 (Q.obj (((CochainComplex.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
⊢ (𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) ≫
        𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X)))) ≫
      ((𝟙
                ((SingleFunctors.postcompFunctor C ℤ Qh).obj
                  ((CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ))))).hom
            n).app
        X =
    𝟙 (Q.obj (((CochainComplex.singleFunctors C).functor n).obj X))

Tactic:
rw [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
⊢ (𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) ≫
        𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X)))) ≫
      𝟙
        ((((SingleFunctors.postcompFunctor C ℤ Qh).obj
                  ((CochainComplex.singleFunctors C).postcomp
                    (HomotopyCategory.quotient C (ComplexShape.up ℤ)))).functor
              n).obj
          X) =
    𝟙 (Q.obj (((CochainComplex.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
                ((CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ)))).functor
            n).obj
        X) =
    𝟙 (Q.obj (((CochainComplex.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
⊢ (𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) ≫
        𝟙
          (Qh.obj
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              (((CochainComplex.singleFunctors C).functor n).obj X)))) ≫
      𝟙
        ((((SingleFunctors.postcompFunctor C ℤ Qh).obj
                  ((CochainComplex.singleFunctors C).postcomp
                    (HomotopyCategory.quotient C (ComplexShape.up ℤ)))).functor
              n).obj
          X) =
    𝟙 (Q.obj (((CochainComplex.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
⊢ 𝟙
      ((((SingleFunctors.postcompFunctor C ℤ Qh).obj
                ((CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ)))).functor
            n).obj
        X) =
    𝟙 (Q.obj (((CochainComplex.singleFunctors C).functor n).obj X))