Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₁ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₁

pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₂ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₂

pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₃ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₃

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₁ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₂ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₃ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₃