awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
dsimp : t.IsLE ((t.truncLT n).obj X) (n - 1)
⊢ t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
⊢ t.IsLE ((t.truncLT n).obj X) (n - 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
dsimp : t.IsGE ((t.truncGE n).obj X) n
⊢ t.IsGE ((t.triangleLTGE n).obj X).obj₃ n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
⊢ t.IsGE ((t.truncGE n).obj X) n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
mp :
  ∀ (e : Triangle.invRotate (contractibleTriangle X) ≅ (t.triangleLTGE n).obj X)
    (he : e.hom.hom₂ = Iso.hom (Iso.refl X)), IsIso ((t.truncGEπ n).app X)
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
obtain ⟨e, he⟩ := t.triangle_iso_exists
      (inv_rot_of_distTriang _ (contractible_distinguished X))
      (t.triangleLTGE_distinguished n X) (Iso.refl X) (n - 1) n
      (t.isLE_of_iso (shiftFunctor C (-1 : ℤ)).mapZeroObject.symm _)
      (by dsimp; infer_instance) (by dsimp; infer_instance) (by dsimp; infer_instance)

Premises used: CategoryTheory.Triangulated.TStructure.triangle_iso_exists, HSub.hSub, CategoryTheory.shiftFunctor, CategoryTheory.Iso.refl, CategoryTheory.Triangulated.TStructure.isLE_of_iso, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapZeroObject, CategoryTheory.Pretriangulated.contractible_distinguished, OfNat.ofNat, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
e : Triangle.invRotate (contractibleTriangle X) ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
⊢ Triangle.mor₂ (Triangle.invRotate (contractibleTriangle X)) ≫ e.hom.hom₃ =
    e.hom.hom₂ ≫ ((t.triangleLTGE n).obj X).mor₂

Tactic:
have := e.hom.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
e : Triangle.invRotate (contractibleTriangle X) ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : 𝟙 X ≫ e.hom.hom₃ = e.hom.hom₂ ≫ (t.truncGEπ n).app X
rw : e.hom.hom₂ ≫ (t.truncGEπ n).app X = e.hom.hom₂ ≫ e.hom.hom₃
rw₁ : 𝟙 X ≫ e.hom.hom₃ = e.hom.hom₂ ≫ e.hom.hom₃
rw₂ rw₃ : 𝟙 X ≫ e.hom.hom₃ = 𝟙 X ≫ e.hom.hom₃
⊢ (t.truncGEπ n).app X = e.hom.hom₃

Tactic:
rw [← cancel_epi e.hom.hom₂, ← this, he]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
e : Triangle.invRotate (contractibleTriangle X) ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
⊢ (t.truncGEπ n).app X = e.hom.hom₃

Tactic:
have : (truncGEπ t n).app X = e.hom.hom₃ := by
      have := e.hom.comm₂
      dsimp at this
      rw [← cancel_epi e.hom.hom₂, ← this, he]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
e : Triangle.invRotate (contractibleTriangle X) ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : (t.truncGEπ n).app X = e.hom.hom₃
mp : IsIso e.hom.hom₃
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
e : Triangle.invRotate (contractibleTriangle X) ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : (t.truncGEπ n).app X = e.hom.hom₃
⊢ IsIso e.hom.hom₃

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : IsIso ((t.truncGEπ n).app X)
⊢ t.IsGE X n

Tactic:
t.isGE_of_iso (asIso ((truncGEπ t n).app X)).symm n

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.Iso.symm, CategoryTheory.NatTrans.app, CategoryTheory.asIso, CategoryTheory.Triangulated.TStructure.truncGEπ
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : IsIso ((t.truncGEπ n).app X)
⊢ t.IsGE X n

Tactic:
exact t.isGE_of_iso (asIso ((truncGEπ t n).app X)).symm n

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.Iso.symm, CategoryTheory.NatTrans.app, CategoryTheory.asIso, CategoryTheory.Triangulated.TStructure.truncGEπ
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
n : ℤ
inst_6 rw : t.IsGE X n
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
rw [← isGE_iff_isIso_truncGEπ_app]

Premises used: CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
n : ℤ
inst_6 : t.IsGE X n
⊢ t.IsGE X n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
rw : IsIso ((t.truncGEπ n).app X) ↔ IsZero.{v, u} ((t.truncLT n).obj X)
⊢ t.IsGE X n ↔ IsZero.{v, u} ((t.truncLT n).obj X)

Tactic:
rw [t.isGE_iff_isIso_truncGEπ_app n X]

Premises used: CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
⊢ IsIso ((t.truncGEπ n).app X) ↔ IsZero.{v, u} ((t.truncLT n).obj X)

Tactic:
(Triangle.isZero₁_iff_isIso₂ _ (t.triangleLTGE_distinguished n X)).symm

Premises used: CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Classical.choose, Iff.symm, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
⊢ IsIso ((t.truncGEπ n).app X) ↔ IsZero.{v, u} ((t.truncLT n).obj X)

Tactic:
exact (Triangle.isZero₁_iff_isIso₂ _ (t.triangleLTGE_distinguished n X)).symm

Premises used: CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Iff.symm, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
rw : IsIso ((t.truncLTι n₁).app X) ↔ IsZero.{v, u} ((t.truncGE n₁).obj X)
⊢ t.IsLE X n₀ ↔ IsZero.{v, u} ((t.truncGE n₁).obj X)

Tactic:
rw [t.isLE_iff_isIso_truncLTι_app n₀ n₁ h X]

Premises used: CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncLTι n₁).app X) ↔ IsZero.{v, u} ((t.truncGE n₁).obj X)

Tactic:
(Triangle.isZero₃_iff_isIso₁ _ (t.triangleLTGE_distinguished n₁ X)).symm

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Classical.choose, Iff.symm
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncLTι n₁).app X) ↔ IsZero.{v, u} ((t.truncGE n₁).obj X)

Tactic:
exact (Triangle.isZero₃_iff_isIso₁ _ (t.triangleLTGE_distinguished n₁ X)).symm

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Iff.symm
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
inst_6 rw : t.IsGE X n
⊢ IsZero.{v, u} ((t.truncLT n).obj X)

Tactic:
rw [← isGE_iff_isZero_truncLT_obj]

Premises used: CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLT_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
inst_6 : t.IsGE X n
⊢ t.IsGE X n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
inst_6 rw : t.IsLE X n₀
⊢ IsZero.{v, u} ((t.truncGE n₁).obj X)

Tactic:
rw [← t.isLE_iff_isZero_truncGE_obj _ _ h X]

Premises used: CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
inst_6 : t.IsLE X n₀
⊢ t.IsLE X n₀

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
this : ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0
rw : f₁ - f₂ = 0
rw₁ rw₂ : Eq.{v + 1} (α := (t.truncGE n).obj X ⟶ Y) 0 0
⊢ f₁ = f₂

Tactic:
rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]

Premises used: sub_eq_zero, HSub.hSub
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
suffices : ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0
⊢ f₁ = f₂

Tactic:
suffices ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0 by
    rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
obtain :
  ∀ (g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁ ⟶ Y)
    (hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g), f = 0
⊢ f = 0

Tactic:
obtain ⟨g, hg⟩ := Triangle.yoneda_exact₃ _
    (t.triangleLTGE_distinguished n X) f hf

Premises used: CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
⊢ n - 2 < n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
⊢ 1 + (n - 2) = n - 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
⊢ t.IsLE (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁) (n - 2)

Tactic:
exact t.isLE_shift _ (n-1) 1 (n-2) (by lia)

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isLE_shift, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
⊢ g = 0

Tactic:
have hg' := t.zero_of_isLE_of_isGE g (n-2) n (by lia)
    (by exact t.isLE_shift _ (n-1) 1 (n-2) (by lia)) inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst_6 : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
hg' : g = 0
rw : ((t.triangleLTGE n).obj X).mor₃ ≫ g = 0
rw₁ : Eq (α := (t.truncGE n).obj X ⟶ Y) (((t.triangleLTGE n).obj X).mor₃ ≫ 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := (t.truncGE n).obj X ⟶ Y) 0 0
⊢ f = 0

Tactic:
rw [hg, hg', comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst_6 : t.IsLE Y (n - 1)
this : ∀ (f : Y ⟶ (t.truncLT n).obj X), f ≫ (t.truncLTι n).app X = 0 → f = 0
rw : f₁ - f₂ = 0
rw₁ rw₂ : Eq.{v + 1} (α := Y ⟶ (t.truncLT n).obj X) 0 0
⊢ f₁ = f₂

Tactic:
rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]

Premises used: sub_eq_zero, HSub.hSub
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst_6 : t.IsLE Y (n - 1)
suffices : ∀ (f : Y ⟶ (t.truncLT n).obj X), f ≫ (t.truncLTι n).app X = 0 → f = 0
⊢ f₁ = f₂

Tactic:
suffices ∀ (f : Y ⟶ (t.truncLT n).obj X) (_ : f ≫ (t.truncLTι n).app X = 0), f = 0 by
    rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst_6 : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
obtain :
  ∀ (g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁) (hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁), f = 0
⊢ f = 0

Tactic:
obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _
    (t.triangleLTGE_distinguished n X)) f hf

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst_6 : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
⊢ n - 1 < n + 1

Tactic:
lia