awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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.triangleLTGE n).obj X).obj₃ n
have dsimp : t.IsGE ((t.truncGE n).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ IsIso ((t.truncGEπ n).app X)
have 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)
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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₃
have this : Triangle.mor₂ (Triangle.invRotate (contractibleTriangle X)) ≫ e.hom.hom₃ = e.hom.hom₂ ≫ ((t.triangleLTGE n).obj X).mor₂
Tactic: have := e.hom.comm₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ (t.truncGEπ n).app X = e.hom.hom₃
have rw : e.hom.hom₂ ≫ (t.truncGEπ n).app X = e.hom.hom₂ ≫ e.hom.hom₃
Tactic: rw [← cancel_epi e.hom.hom₂, ← this, he]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₃
⊢ (t.truncGEπ n).app X = e.hom.hom₃
have rw₁ : 𝟙 X ≫ e.hom.hom₃ = e.hom.hom₂ ≫ e.hom.hom₃
Tactic: rw [← cancel_epi e.hom.hom₂, ← this, he]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₃
⊢ (t.truncGEπ n).app X = e.hom.hom₃
have rw₂ : 𝟙 X ≫ e.hom.hom₃ = 𝟙 X ≫ e.hom.hom₃
Tactic: rw [← cancel_epi e.hom.hom₂, ← this, he]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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
⊢ IsIso ((t.truncGEπ n).app X)
have this : (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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 ((t.truncGEπ n).app X)
have mp : IsIso e.hom.hom₃
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ t.IsGE X n ↔ IsZero.{v, u} ((t.truncLT n).obj X)
have rw : IsIso ((t.truncGEπ n).app X) ↔ IsZero.{v, u} ((t.truncLT n).obj X)
Tactic: rw [t.isGE_iff_isIso_truncGEπ_app n X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ t.IsLE X n₀ ↔ IsZero.{v, u} ((t.truncGE n₁).obj X)
have rw : IsIso ((t.truncLTι n₁).app X) ↔ IsZero.{v, u} ((t.truncGE n₁).obj X)
Tactic: rw [t.isLE_iff_isIso_truncLTι_app n₀ n₁ h X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f₁ = f₂
have rw : f₁ - f₂ = 0
Tactic: rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f₁ = f₂
have rw₁ : Eq.{v + 1} (α := (t.truncGE n).obj X ⟶ Y) 0 0
Tactic: rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₁ = f₂
have suffices : ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0
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)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f = 0
have 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
Tactic: obtain ⟨g, hg⟩ := Triangle.yoneda_exact₃ _
    (t.triangleLTGE_distinguished n X) f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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
⊢ f = 0
have hg' : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f = 0
have rw : ((t.triangleLTGE n).obj X).mor₃ ≫ g = 0
Tactic: rw [hg, hg', comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f = 0
have rw₁ : Eq (α := (t.truncGE n).obj X ⟶ Y) (((t.triangleLTGE n).obj X).mor₃ ≫ 0) 0
Tactic: rw [hg, hg', comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f = 0
have rw₂ : Eq.{v + 1} (α := (t.truncGE n).obj X ⟶ Y) 0 0
Tactic: rw [hg, hg', comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f₁ = f₂
have rw : f₁ - f₂ = 0
Tactic: rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f₁ = f₂
have rw₁ : Eq.{v + 1} (α := Y ⟶ (t.truncLT n).obj X) 0 0
Tactic: rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₁ = f₂
have suffices : ∀ (f : Y ⟶ (t.truncLT n).obj X), f ≫ (t.truncLTι n).app X = 0 → f = 0
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)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ f = 0
have obtain : ∀ (g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁) (hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁), f = 0
Tactic: obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _
    (t.triangleLTGE_distinguished n X)) f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₁
⊢ t.IsGE ((t.triangleLTGE n).obj X).invRotate.obj₁ (n + 1)
have dsimp : t.IsGE (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) ((t.truncGE n).obj X)) (n + 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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₁
⊢ f = 0
have hg' : g = 0
Tactic: have hg' := t.zero_of_isLE_of_isGE g (n - 1) (n + 1) (by lia) inferInstance
    (by dsimp; apply (t.isGE_shift _ n (-1) (n + 1) (by lia)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₁
hg' : g = 0
⊢ f = 0
have rw : g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁ = 0
Tactic: rw [hg, hg', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₁
hg' : g = 0
rw : g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁ = 0
⊢ f = 0
have rw₁ : Eq (α := Y ⟶ (t.truncLT n).obj X) (0 ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁) 0
Tactic: rw [hg, hg', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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₁
hg' : g = 0
rw : g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁ = 0
rw₁ : Eq (α := Y ⟶ (t.truncLT n).obj X) (0 ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁) 0
⊢ f = 0
have rw₂ : Eq.{v + 1} (α := Y ⟶ (t.truncLT n).obj X) 0 0
Tactic: rw [hg, hg', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst_6 : t.IsLE X n₀
⊢ t.IsGE ((t.triangleLTGE n₁).obj Y).obj₃ n₁
have dsimp : t.IsGE ((t.truncGE n₁).obj Y) n₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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 Y : C
f : X ⟶ Y
n : ℤ
inst_6 : t.IsGE Y n
⊢ t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)
have dsimp : t.IsLE ((t.truncLT n).obj X) (n - 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
have refine : ∀ (hX : ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0), t.IsLE X n₀
Tactic: refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
hX : ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
⊢ t.IsLE X n₀
have rw : Eq.{v + 1} (α := (t.truncGE n₁).obj X ⟶ (t.truncGE n₁).obj X) (𝟙 ((t.truncGE n₁).obj X)) 0
Tactic: rw [t.isLE_iff_isZero_truncGE_obj n₀ n₁ h, IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
⊢ t.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
have refine : ∀ (hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0), t.IsGE X n₁
Tactic: refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ t.IsGE X n₁
have rw : Eq.{v + 1} (α := (t.truncLT n₁).obj X ⟶ (t.truncLT n₁).obj X) (𝟙 ((t.truncLT n₁).obj X)) 0
Tactic: rw [t.isGE_iff_isZero_truncLT_obj n₁ X, IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
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
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ t.IsLE ((t.truncLT n₁).obj X) n₀
have rw : t.IsLE ((t.truncLT (n₀ + 1)).obj X) n₀
Tactic: rw [← h]