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
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
ofNat : H (Int.ofNat 0)
ofNat₁ : ∀ (n : ℕ) (hn : H (Int.ofNat n)), H (Int.ofNat (n + 1))
⊢ H (Int.ofNat n)

Tactic:
induction n with
    | zero => exact H_zero
    | succ n hn => exact H_add hn H_one 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
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
⊢ H (Int.negSucc 0)

Tactic:
H_neg_one

Premises used: Set.Mem, Int.add, Int.neg, Int.negOfNat
-- 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
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
⊢ H (Int.negSucc 0)

Tactic:
exact H_neg_one
-- 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
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
hn : H (Int.negSucc n)
⊢ H (Int.negSucc (n + 1))

Tactic:
H_add hn H_neg_one rfl

Premises used: 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
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
hn : H (Int.negSucc n)
⊢ H (Int.negSucc (n + 1))

Tactic:
exact H_add hn H_neg_one rfl

Premises used: 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
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
negSucc : H (Int.negSucc 0)
negSucc₁ : ∀ (n : ℕ) (hn : H (Int.negSucc n)), H (Int.negSucc (n + 1))
⊢ H (Int.negSucc n)

Tactic:
induction n with
    | zero => exact H_neg_one
    | succ n hn => exact H_add hn H_neg_one 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
n : ℤ
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Functor.obj (CategoryTheory.shiftFunctor (Triangle.{v, u} C) n) T) ↔
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T

Tactic:
⟨fun hT ↦ isomorphic_distinguished _ (shift_distinguished _ hT (-n)) _
      ((shiftEquiv (Triangle C) n).unitIso.app T),
    fun hT ↦ shift_distinguished T hT n⟩

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Pretriangulated.Triangle.shift_distinguished, CategoryTheory.shiftFunctor, CategoryTheory.Pretriangulated.Triangle, CategoryTheory.shiftEquiv, CategoryTheory.Pretriangulated.isomorphic_distinguished, Iff.intro, CategoryTheory.Iso.app, CategoryTheory.Functor.obj, 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
h : IsZero.{v, u} T.obj₃
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
rwa rwa₁ rwa₂ rwa₃ : IsZero.{v, u} T.obj₃
⊢ IsIso T.mor₁

Tactic:
rwa [← isZero₃_iff_isIso₁ _ hT]

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁
-- 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
h : IsZero.{v, u} T.obj₃
h_1 : IsIso T.mor₁
⊢ T.mor₁ ≫ (asIso T.mor₁).symm.hom = Iso.hom (Iso.refl T.obj₁) ≫ mor₁ (contractibleTriangle T.obj₁)

Tactic:
simp
-- 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
h : IsZero.{v, u} T.obj₁
rw : IsIso T.rotate.mor₁ ↔ IsIso T.mor₂
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T ↔ IsIso T.mor₂

Tactic:
rw [rotate_distinguished_triangle,
    distinguished_iff_of_isZero₃ _ (Functor.map_isZero (CategoryTheory.shiftFunctor C 1) h)]

Premises used: CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₃, CategoryTheory.Pretriangulated.rotate_distinguished_triangle
-- 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
h : IsZero.{v, u} T.obj₁
⊢ IsIso T.rotate.mor₁ ↔ IsIso T.mor₂

Tactic:
simp
-- 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
h : IsZero.{v, u} T.obj₂
rw : IsIso T.rotate.mor₂ ↔ IsIso T.mor₃
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T ↔ IsIso T.mor₃

Tactic:
rw [rotate_distinguished_triangle, distinguished_iff_of_isZero₁ _ h]

Premises used: CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁, CategoryTheory.Pretriangulated.rotate_distinguished_triangle
-- 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
h : IsZero.{v, u} T.obj₂
⊢ IsIso T.rotate.mor₂ ↔ IsIso T.mor₃

Tactic:
simp
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
obtain :
  ∀ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)),
    IsSplitEpi f
⊢ IsSplitEpi f

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
rw : Eq.{v + 1} (α := (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₃) (𝟙 (Triangle.mk f g h).obj₂ ≫ 0) 0
rw₁ rw₂ : Eq.{v + 1} (α := (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₃) 0 0
⊢ 𝟙 (Triangle.mk f g h).obj₂ ≫ (Triangle.mk f g h).mor₂ = 0

Tactic:
rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
obtain :
  ∀ (r : (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₁)
    (hr : 𝟙 (Triangle.mk f g h).obj₂ = r ≫ (Triangle.mk f g h).mor₁), IsSplitEpi f
⊢ IsSplitEpi f

Tactic:
obtain ⟨r, hr⟩ := Triangle.coyoneda_exact₂ _ hT (𝟙 _)
      (by rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
r : (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₁
hr : 𝟙 (Triangle.mk f g h).obj₂ = r ≫ (Triangle.mk f g h).mor₁
⊢ IsSplitEpi f

Tactic:
⟨r, hr.symm⟩

Premises used: Nonempty.intro, CategoryTheory.SplitEpi.mk, CategoryTheory.IsSplitEpi.mk, Eq.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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
r : (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₁
hr : 𝟙 (Triangle.mk f g h).obj₂ = r ≫ (Triangle.mk f g h).mor₁
⊢ IsSplitEpi f

Tactic:
exact ⟨r, hr.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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Mono f
obtain :
  ∀ (X_1 : C) (g : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X_1)
    (hT :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g f h)),
    IsSplitMono f
⊢ IsSplitMono f

Tactic:
obtain ⟨X, g, h, hT⟩ := distinguished_cocone_triangle₁ f

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
rw : Eq.{v + 1} (α := (Triangle.mk g f h).obj₁ ⟶ (Triangle.mk g f h).obj₂) (0 ≫ 𝟙 (Triangle.mk g f h).obj₂) 0
rw₁ rw₂ : Eq.{v + 1} (α := (Triangle.mk g f h).obj₁ ⟶ (Triangle.mk g f h).obj₂) 0 0
⊢ (Triangle.mk g f h).mor₁ ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0

Tactic:
rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, zero_comp]

Premises used: CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_mono₂, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
obtain :
  ∀ (r : (Triangle.mk g f h).obj₃ ⟶ (Triangle.mk g f h).obj₂)
    (hr : 𝟙 (Triangle.mk g f h).obj₂ = (Triangle.mk g f h).mor₂ ≫ r), IsSplitMono f
⊢ IsSplitMono f

Tactic:
obtain ⟨r, hr⟩ := Triangle.yoneda_exact₂ _ hT (𝟙 _) (by
      rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, zero_comp])

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
r : (Triangle.mk g f h).obj₃ ⟶ (Triangle.mk g f h).obj₂
hr : 𝟙 (Triangle.mk g f h).obj₂ = (Triangle.mk g f h).mor₂ ≫ r
⊢ IsSplitMono f

Tactic:
⟨r, hr.symm⟩

Premises used: CategoryTheory.SplitMono.mk, Nonempty.intro, Eq.symm, CategoryTheory.IsSplitMono.mk
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
r : (Triangle.mk g f h).obj₃ ⟶ (Triangle.mk g f h).obj₂
hr : 𝟙 (Triangle.mk g f h).obj₂ = (Triangle.mk g f h).mor₂ ≫ r
⊢ IsSplitMono f

Tactic:
exact ⟨r, hr.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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
rw : ∀ (P : C) (g : P ⟶ T.obj₂), g ≫ φ.hom₂ = 0 → g = 0
⊢ Mono φ.hom₂

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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₁ : f ≫ T.mor₂ ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₂ : f ≫ φ.hom₂ ≫ T'.mor₂ = 0 ≫ φ.hom₃
rw₃ : Eq (α := A ⟶ T'.obj₃) (0 ≫ T'.mor₂) (0 ≫ φ.hom₃)
rw₄ : Eq (α := A ⟶ T'.obj₃) 0 (0 ≫ φ.hom₃)
rw₅ rw₆ : Eq.{v + 1} (α := A ⟶ T'.obj₃) 0 0
⊢ f ≫ T.mor₂ = 0

Tactic:
rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, CategoryTheory.Pretriangulated.TriangleMorphism.hom₃
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
obtain : ∀ (g : A ⟶ T.obj₁) (hf : (g ≫ T.mor₁) ≫ φ.hom₂ = 0), g ≫ T.mor₁ = 0
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := Triangle.coyoneda_exact₂ _ hT f
      (by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp])

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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : (g ≫ T.mor₁) ≫ φ.hom₂ = 0
⊢ g ≫ T.mor₁ ≫ φ.hom₂ = 0

Tactic:
rw [assoc] at hf

Premises used: CategoryTheory.Category.assoc
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
dsimp : (g ≫ φ.hom₁) ≫ T'.mor₁ = 0
⊢ (g ≫ φ.hom₁) ≫ T'.invRotate.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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
rw : g ≫ φ.hom₁ ≫ T'.mor₁ = 0
rw₁ : g ≫ T.mor₁ ≫ φ.hom₂ = 0
rw₂ rw₃ : Eq.{v + 1} (α := A ⟶ T'.obj₂) 0 0
⊢ (g ≫ φ.hom₁) ≫ T'.mor₁ = 0

Tactic:
rw [assoc, ← φ.comm₁, hf]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁