awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ F.map f.hom₂ = F.map g.hom₂

Tactic:
exact congr_arg TriangleMorphism.hom₂ h

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, congr_arg
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ F.map f.hom₃ = F.map g.hom₃

Tactic:
congr_arg TriangleMorphism.hom₃ h

Premises used: congr_arg, CategoryTheory.Pretriangulated.TriangleMorphism.hom₃
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ F.map f.hom₃ = F.map g.hom₃

Tactic:
exact congr_arg TriangleMorphism.hom₃ h

Premises used: congr_arg, CategoryTheory.Pretriangulated.TriangleMorphism.hom₃
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Full
inst_9 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)
⊢ F.map (X.mor₁ ≫ F.preimage f.hom₂) = F.map (F.preimage f.hom₁ ≫ Y.mor₁)

Tactic:
simpa only [mapTriangle_obj, map_comp, map_preimage] using f.comm₁

Premises used: CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Full
inst_9 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)
⊢ F.map (X.mor₂ ≫ F.preimage f.hom₃) = F.map (F.preimage f.hom₂ ≫ Y.mor₂)

Tactic:
simpa only [mapTriangle_obj, map_comp, map_preimage] using f.comm₂

Premises used: CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Full
inst_9 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)
rw :
  Eq (α := F.obj X.obj₃ ⟶ (F ⋙ shiftFunctor D (A := ℤ) 1).obj Y.obj₁)
    (F.map (X.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) (F.preimage f.hom₁)) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
    (F.map (F.preimage f.hom₃ ≫ Y.mor₃) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
⊢ F.map (X.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) (F.preimage f.hom₁)) = F.map (F.preimage f.hom₃ ≫ Y.mor₃)

Tactic:
rw [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app Y.obj₁)]

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.cancel_mono, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Full
inst_9 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)
⊢ Eq (α := F.obj X.obj₃ ⟶ (F ⋙ shiftFunctor D (A := ℤ) 1).obj Y.obj₁)
    (F.map (X.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) (F.preimage f.hom₁)) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
    (F.map (F.preimage f.hom₃ ≫ Y.mor₃) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)

Tactic:
simpa only [mapTriangle_obj, map_comp, assoc, commShiftIso_hom_naturality,
          map_preimage, Triangle.mk_mor₃] using f.comm₃

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CategoryTheory.Functor.commShiftIso_hom_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.Triangle.mk_mor₃, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
n : ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₁ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ⟶
      Triangle.obj₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T))
    (Triangle.mor₁ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ≫ Iso.hom (Iso.app (commShiftIso F n) T.obj₂))
    (CategoryStruct.comp (Y := Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T))
      (Iso.hom (Iso.app (commShiftIso F n) T.obj₁)) (Triangle.mor₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
n : ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₂ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ⟶
      Triangle.obj₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T))
    (Triangle.mor₂ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ≫ Iso.hom (Iso.app (commShiftIso F n) T.obj₃))
    (CategoryStruct.comp (Y := Triangle.obj₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T))
      (Iso.hom (Iso.app (commShiftIso F n) T.obj₂)) (Triangle.mor₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
n : ℤ
T : Triangle.{v_1, u_1} C
dsimp :
  (F.map
          (HSMul.hSMul (β :=
            obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃ ⟶
              obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁))
            n.negOnePow
            (map (shiftFunctor C n) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) T.obj₁ :
              obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃ ⟶
                obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁))) ≫
        NatTrans.app (Iso.hom (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁)) ≫
      map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₁) =
    NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₃ ≫
      HSMul.hSMul (β :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₃) ⟶
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
        n.negOnePow
        (map (shiftFunctor D n) (F.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₃) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
⊢ Eq (α :=
    Triangle.obj₃ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
        (Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T)))
    (Triangle.mor₃ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ≫
      map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Iso.app (commShiftIso F n) T.obj₁)))
    (CategoryStruct.comp (Y := Triangle.obj₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T))
      (Iso.hom (Iso.app (commShiftIso F n) T.obj₃)) (Triangle.mor₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
n : ℤ
T : Triangle.{v_1, u_1} C
⊢ HSMul.hSMul (β :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (F.map (map (shiftFunctor C n) T.mor₃) ≫
        CategoryStruct.comp (Y :=
          F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁)))
          (CategoryStruct.comp (Y :=
            (F ⋙ shiftFunctor D n).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
            (NatTrans.app (Iso.hom (commShiftIso F n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
            (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
              NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁) ≫
                map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.inv (commShiftIso F n)) T.obj₁) ≫
                  NatTrans.app (Iso.inv (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁)))
          (NatTrans.app (Iso.hom (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁) ≫
            map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₁))) =
    HSMul.hSMul (β :=
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (F.map (map (shiftFunctor C n) T.mor₃) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)))
          (NatTrans.app (Iso.hom (commShiftIso F n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
          (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁)))

Tactic:
simp only [comp_obj, assoc, Iso.inv_hom_id_app_assoc,
        ← Functor.map_comp, Iso.inv_hom_id_app, map_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
w :
  ∀ (x : Triangle.{v_1, u_1} C),
    Eq (α :=
      Triangle.obj₁ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
        Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
      (TriangleMorphism.hom₁ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
      (TriangleMorphism.hom₁
        (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
w₁ :
  ∀ (x : Triangle.{v_1, u_1} C),
    Eq (α :=
      Triangle.obj₂ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
        Triangle.obj₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
      (TriangleMorphism.hom₂ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
      (TriangleMorphism.hom₂
        (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
w₂ :
  ∀ (x : Triangle.{v_1, u_1} C),
    Eq (α :=
      Triangle.obj₃ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
        Triangle.obj₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
      (TriangleMorphism.hom₃ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
      (TriangleMorphism.hom₃
        (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
⊢ Eq (α :=
    Iso (C := Triangle.{v_1, u_1} C ⥤ Triangle.{v_2, u_2} D) (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle)
      (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)))
    (F.mapTriangleCommShiftIso (n + m)) (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
x : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₁ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
      Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
    (TriangleMorphism.hom₁ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
    (TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
x : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₂ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
      Triangle.obj₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
    (TriangleMorphism.hom₂ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
    (TriangleMorphism.hom₂
      (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
x : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₃ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
      Triangle.obj₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
    (TriangleMorphism.hom₃ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
    (TriangleMorphism.hom₃
      (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₁ (obj (F.mapTriangle ⋙ rotate D) T) ≫
      Iso.hom (Iso.refl (Triangle.obj₂ (obj (F.mapTriangle ⋙ rotate D) T))) =
    Iso.hom (Iso.refl (Triangle.obj₁ (obj (F.mapTriangle ⋙ rotate D) T))) ≫
      Triangle.mor₁ (obj (rotate C ⋙ F.mapTriangle) T)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₂ (obj (F.mapTriangle ⋙ rotate D) T) ≫ Iso.hom (Iso.app (Iso.symm (commShiftIso F 1)) T.obj₁) =
    Iso.hom (Iso.refl (Triangle.obj₂ (obj (F.mapTriangle ⋙ rotate D) T))) ≫
      Triangle.mor₂ (obj (rotate C ⋙ F.mapTriangle) T)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₃ (obj (F.mapTriangle ⋙ rotate D) T) ≫
      map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Iso.refl (Triangle.obj₁ (obj (F.mapTriangle ⋙ rotate D) T)))) =
    CategoryStruct.comp (Y := Triangle.obj₃ (obj (rotate C ⋙ F.mapTriangle) T))
      (Iso.hom (Iso.app (Iso.symm (commShiftIso F 1)) T.obj₁)) (Triangle.mor₃ (obj (rotate C ⋙ F.mapTriangle) T))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₁ (obj (F.mapTriangle ⋙ invRotate D) T) ≫
      Iso.hom (Iso.refl (Triangle.obj₂ (obj (F.mapTriangle ⋙ invRotate D) T))) =
    CategoryStruct.comp (Y := Triangle.obj₁ (obj (invRotate C ⋙ F.mapTriangle) T))
      (Iso.hom (Iso.app (Iso.symm (commShiftIso F (-1))) T.obj₃)) (Triangle.mor₁ (obj (invRotate C ⋙ F.mapTriangle) T))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₂ (obj (F.mapTriangle ⋙ invRotate D) T) ≫
      Iso.hom (Iso.refl (Triangle.obj₃ (obj (F.mapTriangle ⋙ invRotate D) T))) =
    Iso.hom (Iso.refl (Triangle.obj₂ (obj (F.mapTriangle ⋙ invRotate D) T))) ≫
      Triangle.mor₂ (obj (invRotate C ⋙ F.mapTriangle) T)

Tactic:
simp