Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: 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 =
    (((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✝

Tactic:
ext

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₃