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 : 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) ≫
      map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Iso.app (Iso.symm (commShiftIso F (-1))) T.obj₃)) =
    Iso.hom (Iso.refl (Triangle.obj₃ (obj (F.mapTriangle ⋙ invRotate D) T))) ≫
      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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_11 : F₁.CommShift ℤ
inst_12 : F₂.CommShift ℤ
inst_13 : NatTrans.CommShift e.hom ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α := Triangle.obj₁ (obj F₁.mapTriangle T) ⟶ Triangle.obj₂ (obj F₂.mapTriangle T))
    (Triangle.mor₁ (obj F₁.mapTriangle T) ≫ Iso.hom (e.app T.obj₂))
    (Iso.hom (e.app T.obj₁) ≫ Triangle.mor₁ (obj 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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_11 : F₁.CommShift ℤ
inst_12 : F₂.CommShift ℤ
inst_13 : NatTrans.CommShift e.hom ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α := Triangle.obj₂ (obj F₁.mapTriangle T) ⟶ Triangle.obj₃ (obj F₂.mapTriangle T))
    (Triangle.mor₂ (obj F₁.mapTriangle T) ≫ Iso.hom (e.app T.obj₃))
    (Iso.hom (e.app T.obj₂) ≫ Triangle.mor₂ (obj 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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_11 : F₁.CommShift ℤ
inst_12 : F₂.CommShift ℤ
inst_13 : NatTrans.CommShift e.hom ℤ
T : Triangle.{v_1, u_1} C
dsimp :
  Eq (α := F₁.obj T.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F₂.obj T.obj₁))
    ((F₁.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F₁ 1)) T.obj₁) ≫
      map (shiftFunctor D (A := ℤ) 1) (e.hom.app T.obj₁))
    (e.hom.app T.obj₃ ≫ F₂.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F₂ 1)) T.obj₁)
⊢ Eq (α :=
    Triangle.obj₃ (obj F₁.mapTriangle T) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (Triangle.obj₁ (obj F₂.mapTriangle T)))
    (Triangle.mor₃ (obj F₁.mapTriangle T) ≫ map (shiftFunctor D (A := ℤ) 1) (Iso.hom (e.app T.obj₁)))
    (Iso.hom (e.app T.obj₃) ≫ Triangle.mor₃ (obj F₂.mapTriangle 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
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_11 : F₁.CommShift ℤ
inst_12 : F₂.CommShift ℤ
inst_13 : NatTrans.CommShift e.hom ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α := F₁.obj T.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F₂.obj T.obj₁))
    ((F₁.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F₁ 1)) T.obj₁) ≫
      map (shiftFunctor D (A := ℤ) 1) (e.hom.app T.obj₁))
    (e.hom.app T.obj₃ ≫ F₂.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F₂ 1)) T.obj₁)

Tactic:
simp only [assoc, NatTrans.shift_app_comm e.hom (1 : ℤ) T.obj₁,
        NatTrans.naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.Triangle.obj₁, OfNat.ofNat, CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_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 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)

Tactic:
IsTriangulated.map_distinguished _ hT

Premises used: CategoryTheory.Functor.IsTriangulated.map_distinguished
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
⊢ Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))

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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
⊢ Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))

Tactic:
have h₁ : (0 : X ⟶ Y) = 0 ≫ 𝟙 0 ≫ 0 := by 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
rw : IsZero.{v_2, u_2} (F.obj 0)
⊢ Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0

Tactic:
rw [← IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
apply :
  IsIso (X := Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
    (Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
⊢ IsZero.{v_2, u_2} (F.obj 0)

Tactic:
apply Triangle.isZero₃_of_isIso₁ _
        (F.map_distinguished _ (contractible_distinguished (0 : C)))

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁, CategoryTheory.Pretriangulated.contractible_distinguished, OfNat.ofNat, CategoryTheory.Functor.map_distinguished
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
dsimp : IsIso (X := F.obj 0) (F.map (𝟙 0))
⊢ IsIso (X := Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
    (Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))

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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
⊢ IsIso (X := F.obj 0) (F.map (𝟙 0))

Tactic:
infer_instance
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
⊢ Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0

Tactic:
have h₂ : 𝟙 (F.obj 0) = 0 := by
      rw [← IsZero.iff_id_eq_zero]
      apply Triangle.isZero₃_of_isIso₁ _
        (F.map_distinguished _ (contractible_distinguished (0 : C)))
      dsimp
      infer_instance
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0) ≫ F.map 0)) 0
rw₃ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0) 0
rw₄ :
  Eq (α := F.obj X ⟶ F.obj Y)
    (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) 0 (F.map 0))) 0
rw₅ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) 0) 0
rw₆ rw₇ : Eq.{v_2 + 1} (α := F.obj X ⟶ F.obj Y) 0 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0

Tactic:
rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
this :
  ∀ (X₁ X₃ : C),
    IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (prodComparison F X₁ X₃)
⊢ ∀ (X₁ X₃ : C), PreservesLimit (pair X₁ X₃) F

Tactic:
have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
this_1 :
  ∀ (X₁ X₃ : C),
    IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (prodComparison F X₁ X₃)
this : ∀ (X₁ X₃ : C), PreservesLimit (pair X₁ X₃) F
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
this_1 :
  ∀ (X₁ X₃ : C),
    IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (prodComparison F X₁ X₃)
this : ∀ (X₁ X₃ : C), PreservesLimit (pair X₁ X₃) F
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
exact ⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
suffices :
  ∀ (X₁ X₃ : C),
    IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (prodComparison F X₁ X₃)
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
suffices ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃) by
    have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
    exact ⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩
-- 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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
dsimp :
  Eq (α := F.obj X₁ ⟶ Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
      (prodComparison F X₁ X₃))
    (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
⊢ Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃)) ≫
      prodComparison F X₁ X₃ =
    𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))) ≫
      Triangle.mor₁ (binaryProductTriangle (F.obj X₁) (F.obj X₃))

Tactic:
dsimp