-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (triangle φ).obj₃) n ⟶
      HomologicalComplex.X
        (Functor.obj
          (G.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
          K)
        n)
    (HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) (triangle φ).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (G.mapHomologicalComplex (ComplexShape.up ℤ)) 1)) K)
        n :
      HomologicalComplex.X (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (triangle φ).obj₃) n ⟶
        HomologicalComplex.X
          (Functor.obj
            (G.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
            K)
          n)
    (HomologicalComplex.Hom.f
        (CategoryStruct.comp (Y :=
          mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          (Iso.hom (mapHomologicalComplexIso φ G) :
            Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
              (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
          (Triangle.mor₃
              (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
            Quiver.Hom (V := CochainComplex.{v_2, u_2, 0} D ℤ)
              (Triangle.obj₃
                (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                  (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} D ℤ) (A := ℤ) 1)
                (Triangle.obj₁
                  (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                    (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))))
        n :
      HomologicalComplex.X (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (triangle φ).obj₃) n ⟶
        HomologicalComplex.X
          (Functor.obj
            (G.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
            K)
          n)
have h : G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
  CategoryStruct.comp (Y :=
    HomologicalComplex.X
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
      n)
    (Iso.hom (mapHomologicalComplexXIso φ G n) :
      G.obj ((mappingCone φ).X n) ⟶
        HomologicalComplex.X
          (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (HomologicalComplex.Hom.f
        (Triangle.mor₃
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
        n :
      HomologicalComplex.X
          (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n ⟶
        HomologicalComplex.X
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K))
          n)
Tactic: dsimp [mapHomologicalComplexIso]