-- 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)
            (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₁))))
have dsimp : 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₁))))
Tactic: dsimp