-- 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
⊢ 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