-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Abelian.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
      (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
      (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ)))))
    (CategoryStruct.comp (Y :=
        mappingCone (F := Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₁)
          (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) S.f))
        (Iso.hom (mapHomologicalComplexIso S.f F) :
          Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
            (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
            (mappingCone (F := Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₁)
              (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) S.f)))
        (descShortComplex (S.map (F.mapHomologicalComplex (up ℤ))) :
          Quiver.Hom (V := CochainComplex.{v_2, u_2, 0} D ℤ)
            (mappingCone (F := ShortComplex.X₁ (S.map (F.mapHomologicalComplex (up ℤ))))
              (ShortComplex.f (S.map (F.mapHomologicalComplex (up ℤ)))))
            (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ))))) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
        (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
        (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ)))))
    (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) (descShortComplex S) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
        (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
        (Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₃))
have symm : Eq (α :=
  Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
    (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
    (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ)))))
  (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) (descShortComplex S) :
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
      (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
      (Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₃))
  (CategoryStruct.comp (Y :=
      mappingCone (F := Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₁)
        (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) S.f))
      (Iso.hom (mapHomologicalComplexIso S.f F) :
        Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
          (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
          (mappingCone (F := Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₁)
            (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) S.f)))
      (descShortComplex (S.map (F.mapHomologicalComplex (up ℤ))) :
        Quiver.Hom (V := CochainComplex.{v_2, u_2, 0} D ℤ)
          (mappingCone (F := ShortComplex.X₁ (S.map (F.mapHomologicalComplex (up ℤ))))
            (ShortComplex.f (S.map (F.mapHomologicalComplex (up ℤ)))))
          (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ))))) :
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
      (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
      (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ)))))
Tactic: symm