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
X : C
f : T.obj₃ ⟶ X
hf : T.mor₂ ≫ f = 0
⊢ ∃ (g : Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ X), f = T.mor₃ ≫ g

Tactic:
yoneda_exact₂ _ (rot_of_distTriang _ hT) f hf

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, 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
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
obtain :
  ∀ (a : obj₁.{v, u} (contractibleTriangle X) ⟶ T.obj₁) (ha₁ : mor₁ (contractibleTriangle X) ≫ f = a ≫ T.mor₁),
    mor₃ (contractibleTriangle X) ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) a = 0 ≫ T.mor₃ →
      ∃ (g : X ⟶ T.obj₁), f = g ≫ T.mor₁
⊢ ∃ (g : X ⟶ T.obj₁), f = g ≫ T.mor₁

Tactic:
obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ T
    (contractible_distinguished X) hT f 0 (by cat_disch)

Premises used: CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁, CategoryTheory.Pretriangulated.contractible_distinguished, OfNat.ofNat
-- 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
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : obj₁.{v, u} (contractibleTriangle X) ⟶ T.obj₁
ha₁ : mor₁ (contractibleTriangle X) ≫ f = a ≫ T.mor₁
right : mor₃ (contractibleTriangle X) ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) a = 0 ≫ T.mor₃
⊢ f = a ≫ T.mor₁

Tactic:
simpa using ha₁
-- 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
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : obj₁.{v, u} (contractibleTriangle X) ⟶ T.obj₁
ha₁ : mor₁ (contractibleTriangle X) ≫ f = a ≫ T.mor₁
right : mor₃ (contractibleTriangle X) ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) a = 0 ≫ T.mor₃
⊢ ∃ (g : X ⟶ T.obj₁), f = g ≫ T.mor₁

Tactic:
exact ⟨a, by simpa using ha₁⟩
-- 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
X : C
f : X ⟶ T.obj₃
hf : f ≫ T.mor₃ = 0
⊢ ∃ (g : X ⟶ T.obj₂), f = g ≫ T.mor₂

Tactic:
coyoneda_exact₂ _ (rot_of_distTriang _ hT) f hf

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, 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
mp : T.mor₃ = 0 → Epi T.mor₂
mpr : Epi T.mor₂ → T.mor₃ = 0
⊢ T.mor₃ = 0 ↔ Epi T.mor₂

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 : T.mor₃ = 0
mp : ∀ (R : C) (g : T.obj₃ ⟶ R), T.mor₂ ≫ g = 0 → g = 0
⊢ Epi T.mor₂

Tactic:
rw [epi_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.epi_iff_cancel_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
X : C
g : T.obj₃ ⟶ X
hg : T.mor₂ ≫ g = 0
mp :
  ∀ (f : Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ X) (hg : T.mor₂ ≫ T.mor₃ ≫ f = 0),
    T.mor₃ ≫ f = 0
⊢ g = 0

Tactic:
obtain ⟨f, rfl⟩ := yoneda_exact₃ T hT g hg

Premises used: rfl, CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃
-- 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
X : C
f : Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ X
hg : T.mor₂ ≫ T.mor₃ ≫ f = 0
mp : Eq (α := T.obj₃ ⟶ X) (0 ≫ f) 0
mp₁ mp₂ : Eq.{v + 1} (α := T.obj₃ ⟶ X) 0 0
⊢ T.mor₃ ≫ f = 0

Tactic:
rw [h, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- 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 : Epi T.mor₂
mpr : T.mor₂ ≫ T.mor₃ = T.mor₂ ≫ 0
mpr₁ : Eq (α := T.obj₂ ⟶ Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) 0 (T.mor₂ ≫ 0)
mpr₂ mpr₃ : Eq.{v + 1} (α := T.obj₂ ⟶ Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) 0 0
⊢ T.mor₃ = 0

Tactic:
rw [← cancel_epi T.mor₂, comp_distTriang_mor_zero₂₃ _ hT, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CategoryTheory.Pretriangulated.Triangle.mor₂, CategoryTheory.cancel_epi
-- 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
⊢ T.invRotate.mor₃ = 0 ↔ Epi T.invRotate.mor₂

Tactic:
have h := mor₃_eq_zero_iff_epi₂ _ (inv_rot_of_distTriang _ hT)
-- 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 (α :=
      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₃))
      (T.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.3) 0 ↔
    Epi T.mor₁
rw :
  T.mor₂ = 0 ↔
    Eq (α :=
      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₃))
      (T.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.3) 0
rw₁ rw₂ : T.mor₂ = 0 ↔ T.mor₂ = 0
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Tactic:
rw [← h, IsIso.comp_right_eq_zero]

Premises used: CategoryTheory.Preadditive.IsIso.comp_right_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
⊢ T.rotate.mor₃ = 0 ↔ Epi T.rotate.mor₂

Tactic:
have h := mor₃_eq_zero_iff_epi₂ _ (rot_of_distTriang _ hT)
-- 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₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₂)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.mor₁) 0 ↔
    Epi T.mor₃
rw :
  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) T.obj₂)
      (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.mor₁) 0
⊢ T.mor₁ = 0 ↔ Epi T.mor₃

Tactic:
rw [← h, neg_eq_zero]

Premises used: neg_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
h :
  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) T.obj₂)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.mor₁) 0 ↔
    Epi 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) 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
-- 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₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₂)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.mor₁) 0 ↔
    Epi 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) 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
-- 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 : Epi T.mor₂
⊢ T.mor₃ = 0

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

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂
-- 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 : Epi T.mor₁
⊢ T.mor₂ = 0

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

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁
-- 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 : Epi T.mor₃
⊢ T.mor₁ = 0

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

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃
-- 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
⊢ Epi T.mor₂

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

Premises used: CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂, Iff.mp
-- 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
⊢ Epi T.mor₁

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

Premises used: CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁, Iff.mp
-- 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
⊢ Epi T.mor₃

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

Premises used: Iff.mp, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃
-- 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 → Mono T.mor₂
mpr : Mono T.mor₂ → T.mor₁ = 0
⊢ T.mor₁ = 0 ↔ Mono T.mor₂

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 : T.mor₁ = 0
mp : ∀ (P : C) (g : P ⟶ T.obj₂), g ≫ T.mor₂ = 0 → g = 0
⊢ Mono T.mor₂

Tactic:
rw [mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_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
X : C
g : X ⟶ T.obj₂
hg : g ≫ T.mor₂ = 0
mp : ∀ (f : X ⟶ T.obj₁) (hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0), f ≫ T.mor₁ = 0
⊢ g = 0

Tactic:
obtain ⟨f, rfl⟩ := coyoneda_exact₂ T hT g hg

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, rfl
-- 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
X : C
f : X ⟶ T.obj₁
hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0
mp : Eq (α := X ⟶ T.obj₂) (f ≫ 0) 0
mp₁ mp₂ : Eq.{v + 1} (α := X ⟶ T.obj₂) 0 0
⊢ f ≫ 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 : Mono T.mor₂
mpr : T.mor₁ ≫ T.mor₂ = 0 ≫ T.mor₂
mpr₁ : Eq (α := T.obj₁ ⟶ T.obj₃) 0 (0 ≫ T.mor₂)
mpr₂ mpr₃ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₃) 0 0
⊢ T.mor₁ = 0

Tactic:
rw [← cancel_mono T.mor₂, comp_distTriang_mor_zero₁₂ _ hT, zero_comp]

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.cancel_mono, CategoryTheory.Pretriangulated.Triangle.mor₂, CategoryTheory.Limits.zero_comp
-- 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
⊢ T.mor₂ = 0 ↔ Mono T.mor₃

Tactic:
mor₁_eq_zero_iff_mono₂ _ (rot_of_distTriang _ hT)

Premises used: CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂, 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
⊢ T.invRotate.mor₁ = 0 ↔ Mono T.invRotate.mor₂

Tactic:
have h := mor₁_eq_zero_iff_mono₂ _ (inv_rot_of_distTriang _ hT)
-- 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₁
rw :
  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
⊢ T.mor₃ = 0 ↔ Mono T.mor₁

Tactic:
rw [← h, neg_eq_zero, IsIso.comp_right_eq_zero]

Premises used: CategoryTheory.Preadditive.IsIso.comp_right_eq_zero, neg_eq_zero