Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: case h₁
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₁ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₁

pp: case h₂
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₂ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₂

pp: case h₃
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₃ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₃

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₁ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₁

case h₂
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₂ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₂

case h₃
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₃ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₃