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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₁ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₁

pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₂ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₂

pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₃

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₁ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₂ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₃