-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
refine_3 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁) ≫
      𝟙 (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
refine_3₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
refine_3₂ refine_3₃ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (𝟙 (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)

Tactic:
rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Functor.map_id