Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₁ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₁

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₂ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₂

pp: case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₃ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₃

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₁ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₁

case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₂ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₂

case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₃ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₃