-- 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 S.X₃))
      (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 (triangleOfSESδ hS))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) 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₁)))
        (triangleOfSESδ ⋯)
        (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₃ ≫
      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)
          (Pretriangulated.Triangle.obj₁
            (CochainComplex.mappingCone.triangle (K :=
              ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
              (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))))
      (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 :=
                ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))) :
            Quiver.Hom (V := CochainComplex.{v', u', 0} D ℤ)
              (Pretriangulated.Triangle.obj₃
                (CochainComplex.mappingCone.triangle (K :=
                  ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                  (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))
              (Functor.obj (shiftFunctor (CochainComplex.{v', u', 0} D ℤ) (A := ℤ) 1)
                (Pretriangulated.Triangle.obj₁
                  (CochainComplex.mappingCone.triangle (K :=
                    ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))
                    (ShortComplex.f (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))))))
      (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (Functor.obj Q (ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso Q 1))
          (ShortComplex.X₁ (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))))
        (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 [← cancel_epi (F.mapDerivedCategory.map
    (Q.map (CochainComplex.mappingCone.descShortComplex S))), ← Functor.map_comp,
    descShortComplex_triangleOfSESδ, F.mapDerivedCategoryFactors_hom_naturality_assoc,
    ← CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex,
    Functor.map_comp_assoc, descShortComplex_triangleOfSESδ_assoc, Category.assoc,
    ← Functor.map_comp_assoc]