-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
h₁ :
  Eq (α :=
    (Functor.obj
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
          X).X₁ ⟶
      (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') Y).X₁)
    (ShortComplex.Hom.τ₁
      (CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k) f ≫
        Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            Y)))
    (ShortComplex.Hom.τ₁
      (Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            X) ≫
        CategoryTheory.Functor.map (shortComplexFunctor' C (up ℤ) i' j' k') f))
⊢ Eq (α :=
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
        X ⟶
      Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') Y)
    (CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k) f ≫
      Iso.hom
        ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
            (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
              Functor.obj
                  (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                    shortComplexFunctor' C (up ℤ) i j k)
                  K ≅
                Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
          Y))
    (Iso.hom
        ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
            (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
              Functor.obj
                  (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                    shortComplexFunctor' C (up ℤ) i j k)
                  K ≅
                Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
          X) ≫
      CategoryTheory.Functor.map (shortComplexFunctor' C (up ℤ) i' j' k') f)
have h₂ : Eq (α :=
  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
        X).X₂ ⟶
    (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') Y).X₂)
  (ShortComplex.Hom.τ₂
    (CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k) f ≫
      Iso.hom
        ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
            (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) sorry sorry :
              Functor.obj
                  (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                    shortComplexFunctor' C (up ℤ) i j k)
                  K ≅
                Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
          Y)))
  (ShortComplex.Hom.τ₂
    (Iso.hom
        ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
            (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) sorry sorry :
              Functor.obj
                  (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                    shortComplexFunctor' C (up ℤ) i j k)
                  K ≅
                Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
          X) ≫
      CategoryTheory.Functor.map (shortComplexFunctor' C (up ℤ) i' j' k') f))
Tactic: ext