-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasDerivedCategory.{t, v, u} C
inst_8 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj Q (CochainComplex.mappingCone S.f)))
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁))))
    (Functor.map F.mapDerivedCategory
      (Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) (CochainComplex.mappingCone S.f) ≫
      CategoryStruct.comp (Y :=
        Functor.obj Q
          (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
        (Functor.map Q
          (CategoryStruct.comp (Y :=
            CochainComplex.mappingCone (F := Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
              (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f))
            (Iso.hom (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F) :
              Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) (CochainComplex.mappingCone S.f))
                (CochainComplex.mappingCone (F := Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
                  (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f)))
            (Pretriangulated.Triangle.mor₃
                (CochainComplex.mappingCone.triangle (K :=
                  Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
                  (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f)) :
              Quiver.Hom (V := CochainComplex.{v', u', 0} D ℤ)
                (Pretriangulated.Triangle.obj₃
                  (CochainComplex.mappingCone.triangle (K :=
                    Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
                    (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f)))
                (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
                  (Pretriangulated.Triangle.obj₁
                    (CochainComplex.mappingCone.triangle (K :=
                      Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)
                      (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.f)))))))
        (CategoryStruct.comp (Y :=
          Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
            (Functor.obj Q (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
          (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁))
          (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors) S.X₁) ≫
            NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1)) (Functor.obj Q S.X₁))))
have rw : Eq.{t' + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
    (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
      (Functor.obj Q (CochainComplex.mappingCone S.f)))
    (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
      (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁))))
  (Functor.map F.mapDerivedCategory (Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
    Functor.map F.mapDerivedCategory (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁))
  (Functor.map F.mapDerivedCategory (Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
    NatTrans.app (Iso.hom F.mapDerivedCategoryFactors)
        (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1)
          (CochainComplex.mappingCone.triangle S.f).obj₁) ≫
      CategoryStruct.comp (Y :=
        Functor.obj Q
          (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
        (Functor.map Q
          (NatTrans.app (Iso.hom (Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1)) S.X₁))
        (CategoryStruct.comp (Y :=
          Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
            (Functor.obj Q (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
          (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁))
          (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors) S.X₁) ≫
            NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1)) (Functor.obj Q S.X₁))))
Tactic: rw [← CochainComplex.mappingCone.map_δ, Functor.map_comp_assoc,
    ← F.mapDerivedCategoryFactors_hom_naturality_assoc, Functor.map_comp]