-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
x : X ⟶ Y
i : ℤ
⊢ Eq (α :=
    HomologicalComplex.X
        (obj
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          X)
        i ⟶
      HomologicalComplex.X
        (obj
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
          Y)
        i)
    (HomologicalComplex.Hom.f
      (map
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          x ≫
        Iso.hom
          ((fun (K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ↦
              (HomologicalComplex.Hom.isoOfComponents
                  (fun (x : ℤ) ↦
                    Iso.refl
                      (HomologicalComplex.X
                        (obj
                          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                            F.mapHomologicalComplex (ComplexShape.up ℤ))
                          K)
                        x))
                  ⋯ :
                Iso (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                  (obj
                    (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                      F.mapHomologicalComplex (ComplexShape.up ℤ))
                    K)
                  (obj
                    (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                      shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
                    K)))
            Y))
      i)
    (HomologicalComplex.Hom.f
      (Iso.hom
          ((fun (K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ↦
              (HomologicalComplex.Hom.isoOfComponents
                  (fun (x : ℤ) ↦
                    Iso.refl
                      (HomologicalComplex.X
                        (obj
                          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                            F.mapHomologicalComplex (ComplexShape.up ℤ))
                          K)
                        x))
                  ⋯ :
                Iso (C := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
                  (obj
                    (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
                      F.mapHomologicalComplex (ComplexShape.up ℤ))
                    K)
                  (obj
                    (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
                      shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
                    K)))
            X) ≫
        map
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
          x)
      i)
have h : F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = 𝟙 (F.obj (X.X (i + n))) ≫ F.map (x.f (i + n))
Tactic: dsimp