awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
⊢ HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
      (a + b).negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
        NatTrans.app (Iso.hom (shiftFunctorComm C 1 (a + b))) T.obj₁ ≫
          Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₁)) =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
      (b.negOnePow * a.negOnePow)
      (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₃ ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) ≫
          Functor.map (CategoryTheory.shiftFunctor C b) (NatTrans.app (Iso.hom (shiftFunctorComm C 1 a)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 b))
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Int.negOnePow_add,
          shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, add_comm a]

Premises used: CategoryTheory.shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, Int.negOnePow_add, add_comm, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).mor₁ ≫
      Iso.hom (Iso.refl (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).obj₂) =
    Iso.hom (Iso.refl (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).obj₁) ≫
      (Functor.obj (Triangle.shiftFunctor C 1) T).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).mor₂ ≫
      Iso.hom (Iso.refl (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).obj₃) =
    Iso.hom (Iso.refl (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).obj₂) ≫
      (Functor.obj (Triangle.shiftFunctor C 1) T).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.refl (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).obj₁)) =
    Iso.hom (Iso.refl (Functor.obj (rotate C ⋙ rotate C ⋙ rotate C) T).obj₃) ≫
      (Functor.obj (Triangle.shiftFunctor C 1) T).mor₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).mor₁ ≫
      Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₂) =
    Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₁) ≫
      (Functor.obj (Triangle.shiftFunctor C (-1)) T).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).mor₂ ≫
      Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₃) =
    Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₂) ≫
      (Functor.obj (Triangle.shiftFunctor C (-1)) T).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
dsimp :
  ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C 1 (-1) 0 ⋯)) T.obj₁ ≫
              NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) T.obj₁) ≫
        NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) T.obj₁ ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C (-1) 1 0 ⋯)) T.obj₁) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁)) =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃) ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁))
        (Int.negOnePow (-1))
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 (-1))) T.obj₁ :
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
            Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁))
⊢ (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₁)) =
    Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₃) ≫
      (Functor.obj (Triangle.shiftFunctor C (-1)) T).mor₃

Tactic:
dsimp [shiftFunctorCompIsoId]

Premises used: CategoryTheory.shiftFunctorCompIsoId
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C 1 (-1) 0 ⋯)) T.obj₁ ≫
              NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) T.obj₁) ≫
        NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) T.obj₁ ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C (-1) 1 0 ⋯)) T.obj₁) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁)) =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃) ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁))
        (Int.negOnePow (-1))
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 (-1))) T.obj₁ :
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
            Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁))

Tactic:
simp [shiftFunctorComm_eq C _ _ _ (add_neg_cancel (1 : ℤ))]

Premises used: add_neg_cancel, CategoryTheory.shiftFunctorComm_eq, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
h₁ :
  TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₁
h₂ :
  TriangleMorphism.hom₂
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₂
h₃ :
  TriangleMorphism.hom₃
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₃
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
h₁ :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T.obj₁ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₁) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
    (TriangleMorphism.hom₁ (eqToHom ⋯) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T.obj₁ ≫
          NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C b c (b + c) ⋯))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
⊢ TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
    (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c)) T.obj₁ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C a b)) T.obj₁) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + (b + c))) T.obj₁)
        (TriangleMorphism.hom₁ (eqToHom ⋯))
        (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c)) T.obj₁ ≫
          Functor.map (CategoryTheory.shiftFunctor C c)
            (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C a b)) T.obj₁)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
h₂ :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T.obj₂ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
    (TriangleMorphism.hom₂ (eqToHom ⋯) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T.obj₂ ≫
          NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C b c (b + c) ⋯))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
⊢ TriangleMorphism.hom₂
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
    (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c)) T.obj₂ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C a b)) T.obj₂) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + (b + c))) T.obj₂)
        (TriangleMorphism.hom₂ (eqToHom ⋯))
        (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c)) T.obj₂ ≫
          Functor.map (CategoryTheory.shiftFunctor C c)
            (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C a b)) T.obj₂)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
h₃ :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T.obj₃ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (TriangleMorphism.hom₃ (eqToHom ⋯) ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T.obj₃ ≫
          NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C b c (b + c) ⋯))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
⊢ TriangleMorphism.hom₃
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c)) T.obj₃ ≫
        Functor.map (CategoryTheory.shiftFunctor C c)
          (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C a b)) T.obj₃) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + (b + c))) T.obj₃)
        (TriangleMorphism.hom₃ (eqToHom ⋯))
        (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c)) T.obj₃ ≫
          Functor.map (CategoryTheory.shiftFunctor C c)
            (NatTrans.app (Iso.hom (eqToIso ⋯ ≪≫ shiftFunctorAdd C a b)) T.obj₃)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
n : ℤ
⊢ Eq (α := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) n) (shiftFunctor C n)

Tactic:
rfl

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Pretriangulated.Triangle.shiftFunctor, Int.add, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
⊢ Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) (A := ℤ) 0)
      (𝟭 (Triangle.{v, u} C)))
    (CategoryTheory.shiftFunctorZero (Triangle.{v, u} C) ℤ) (shiftFunctorZero C)

Tactic:
ShiftMkCore.shiftFunctorZero_eq _

Premises used: CategoryTheory.ShiftMkCore.shiftFunctorZero_eq, CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
⊢ Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) (a + b))
      (CategoryTheory.shiftFunctor (Triangle.{v, u} C) a ⋙ CategoryTheory.shiftFunctor (Triangle.{v, u} C) b))
    (shiftFunctorAdd (Triangle.{v, u} C) a b) (shiftFunctorAdd' C a b (a + b) ⋯)

Tactic:
ShiftMkCore.shiftFunctorAdd_eq _ _ _

Premises used: CategoryTheory.shiftFunctor, Int.add.match_1, CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd', CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq, Int.add, CategoryTheory.NatIso.ofComponents