awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h :
  Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ↔
    Mono T.mor₁
⊢ T.mor₃ = 0 ↔
    Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁))
      (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃) 0

Tactic:
(Functor.map_eq_zero_iff (CategoryTheory.shiftFunctor C (-1))).symm

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_eq_zero_iff, OfNat.ofNat, Iff.symm, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h :
  Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ↔
    Mono T.mor₁
⊢ T.mor₃ = 0 ↔
    Eq (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁))
      (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃) 0

Tactic:
exact (Functor.map_eq_zero_iff (CategoryTheory.shiftFunctor C (-1))).symm

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_eq_zero_iff, OfNat.ofNat, Iff.symm, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : Mono T.mor₂
⊢ T.mor₁ = 0

Tactic:
(T.mor₁_eq_zero_iff_mono₂ hT).2 h

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : Mono T.mor₃
⊢ T.mor₂ = 0

Tactic:
(T.mor₂_eq_zero_iff_mono₃ hT).2 h

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : Mono T.mor₁
⊢ T.mor₃ = 0

Tactic:
(T.mor₃_eq_zero_iff_mono₁ hT).2 h

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₁ = 0
⊢ Mono T.mor₂

Tactic:
(T.mor₁_eq_zero_iff_mono₂ hT).1 h

Premises used: Iff.mp, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₂ = 0
⊢ Mono T.mor₃

Tactic:
(T.mor₂_eq_zero_iff_mono₃ hT).1 h

Premises used: Iff.mp, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₃ = 0
⊢ Mono T.mor₁

Tactic:
(T.mor₃_eq_zero_iff_mono₁ hT).1 h

Premises used: Iff.mp, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : IsZero.{v, u} T.obj₂ → T.mor₁ = 0 ∧ T.mor₂ = 0
mpr : T.mor₁ = 0 ∧ T.mor₂ = 0 → IsZero.{v, u} T.obj₂
⊢ IsZero.{v, u} T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : IsZero.{v, u} T.obj₂
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, And.intro, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : IsZero.{v, u} T.obj₂
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
rw : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₃) (𝟙 T.obj₂ ≫ 0) 0
rw₁ rw₂ : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₃) 0 0
⊢ 𝟙 T.obj₂ ≫ T.mor₂ = 0

Tactic:
rw [h₂, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
mpr : ∀ (f : T.obj₂ ⟶ T.obj₁) (hf : 𝟙 T.obj₂ = f ≫ T.mor₁), IsZero.{v, u} T.obj₂
⊢ IsZero.{v, u} T.obj₂

Tactic:
obtain ⟨f, hf⟩ := coyoneda_exact₂ T hT (𝟙 _) (by rw [h₂, comp_zero])

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
f : T.obj₂ ⟶ T.obj₁
hf : 𝟙 T.obj₂ = f ≫ T.mor₁
mpr : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) (𝟙 T.obj₂) 0
mpr₁ : f ≫ T.mor₁ = 0
mpr₂ : Eq (α := T.obj₂ ⟶ T.obj₂) (f ≫ 0) 0
mpr₃ mpr₄ : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) 0 0
⊢ IsZero.{v, u} T.obj₂

Tactic:
rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ IsZero.{v, u} T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
(isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₂_iff, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Iff.trans
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
refine : T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ IsZero.{v, u} T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
refine (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₂_iff, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Iff.trans
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
dsimp :
  Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
        (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
        (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ∧
      T.mor₁ = 0 ↔
    T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
simp : T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
        (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
        (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ∧
      T.mor₁ = 0 ↔
    T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]

Premises used: CategoryTheory.Preadditive.IsIso.comp_right_eq_zero, neg_eq_zero, CategoryTheory.Functor.map_eq_zero_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mp₁ mp₂ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mp₃ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0
mp₄ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₃ = 0
mpr₁ mpr₂ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mpr₃ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0
mpr₄ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₁ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ IsZero.{v, u} T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
(isZero₂_iff _ (rot_of_distTriang _ hT)).trans ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₂_iff, Iff.trans, CategoryTheory.Pretriangulated.rot_of_distTriang
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
refine : T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
⊢ IsZero.{v, u} T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
refine (isZero₂_iff _ (rot_of_distTriang _ hT)).trans ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₂_iff, Iff.trans, CategoryTheory.Pretriangulated.rot_of_distTriang
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
dsimp : T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
⊢ T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₂ = 0 ∧ T.mor₃ = 0 → T.mor₂ = 0 ∧ T.mor₃ = 0
mpr : T.mor₂ = 0 ∧ T.mor₃ = 0 → T.mor₂ = 0 ∧ T.mor₃ = 0
mp₁ mp₂ : T.mor₂ = 0 → T.mor₃ = 0 → T.mor₂ = 0 ∧ T.mor₃ = 0
mp₃ : T.mor₂ = 0 → T.mor₃ = 0 → T.mor₂ = 0
mp₄ : T.mor₂ = 0 → T.mor₃ = 0 → T.mor₃ = 0
mpr₁ mpr₂ : T.mor₂ = 0 → T.mor₃ = 0 → T.mor₂ = 0 ∧ T.mor₃ = 0
mpr₃ : T.mor₂ = 0 → T.mor₃ = 0 → T.mor₂ = 0
mpr₄ : T.mor₂ = 0 → T.mor₃ = 0 → T.mor₃ = 0
⊢ T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₂ : IsZero.{v, u} T.obj₂
h₃ : IsZero.{v, u} T.obj₃
rw : T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ IsZero.{v, u} T.obj₁

Tactic:
rw [T.isZero₁_iff hT]

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₁_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₂ : IsZero.{v, u} T.obj₂
h₃ : IsZero.{v, u} T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
⟨h₂.eq_of_tgt _ _, h₃.eq_of_src _ _⟩

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, And.intro, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₂ : IsZero.{v, u} T.obj₂
h₃ : IsZero.{v, u} T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
exact ⟨h₂.eq_of_tgt _ _, h₃.eq_of_src _ _⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : IsZero.{v, u} T.obj₁
h₃ : IsZero.{v, u} T.obj₃
rw : T.mor₁ = 0 ∧ T.mor₂ = 0
⊢ IsZero.{v, u} T.obj₂

Tactic:
rw [T.isZero₂_iff hT]

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₂_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : IsZero.{v, u} T.obj₁
h₃ : IsZero.{v, u} T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
⟨h₁.eq_of_src _ _, h₃.eq_of_tgt _ _⟩

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, And.intro, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : IsZero.{v, u} T.obj₁
h₃ : IsZero.{v, u} T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
exact ⟨h₁.eq_of_src _ _, h₃.eq_of_tgt _ _⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : IsZero.{v, u} T.obj₁
h₂ : IsZero.{v, u} T.obj₂
dsimp : IsZero.{v, u} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
⊢ IsZero.{v, u} T.rotate.obj₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : IsZero.{v, u} T.obj₁
h₂ : IsZero.{v, u} T.obj₂
simp :
  ∀ (h₁ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₁) (𝟙 T.obj₁) 0),
    Eq.{v + 1} (α :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
      (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)) 0
⊢ IsZero.{v, u} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)

Tactic:
simp only [IsZero.iff_id_eq_zero] at h₁ ⊢

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero