awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
a : ℤ
⊢ IsIso ((t.truncLE a).map f) ↔
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) ((t.truncLE a).obj X))
      (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLEι a).app X ≫ f) g h)),
      t.IsGE Z (a + 1)

Tactic:
apply isIso_truncLT_map_iff

Premises used: CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_iff
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
n : ℤ
⊢ IsIso ((t.truncGT n).map g) ↔
    ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGT n).obj Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_
      :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f (g ≫ (t.truncGTπ n).app Z) h)),
      t.IsLE X n

Tactic:
t.isIso_truncGE_map_iff g n (n + 1) rfl

Premises used: Set.Mem, HAdd.hAdd, OfNat.ofNat, rfl, CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
a b : ℤ
inst_6 : t.IsLE X b
dsimp : t.IsLE ((t.truncLT (a + 1)).obj X) b
⊢ t.IsLE ((t.truncLE a).obj X) b

Tactic:
dsimp [truncLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncLE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
a b : ℤ
inst_6 : t.IsLE X b
⊢ t.IsLE ((t.truncLT (a + 1)).obj X) b

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
a b : ℤ
inst_6 : t.IsGE X a
dsimp : t.IsGE ((t.truncGE (b + 1)).obj X) a
⊢ t.IsGE ((t.truncGT b).obj X) a

Tactic:
dsimp [truncGT]

Premises used: CategoryTheory.Triangulated.TStructure.truncGT
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
a b : ℤ
inst_6 : t.IsGE X a
⊢ t.IsGE ((t.truncGE (b + 1)).obj X) a

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
a b : ℤ
dsimp : t.IsGE ((t.truncGE a).obj ((t.truncLE b).obj X)) a
⊢ t.IsGE ((t.truncGELE a b).obj X) a

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

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsGE T.obj₃ (n₀ + 1)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₃ : t.IsGE T.obj₃ (n₀ + 1)
⊢ IsIso ((t.truncLE n₀).map T.mor₁)

Tactic:
t.isIso₁_truncLT_map_of_isGE _ hT _ h₃

Premises used: CategoryTheory.Triangulated.TStructure.isIso₁_truncLT_map_of_isGE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₃ : t.IsGE T.obj₃ (n₀ + 1)
⊢ IsIso ((t.truncLE n₀).map T.mor₁)

Tactic:
exact t.isIso₁_truncLT_map_of_isGE _ hT _ h₃

Premises used: CategoryTheory.Triangulated.TStructure.isIso₁_truncLT_map_of_isGE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
⊢ IsIso ((t.truncGT n₀).map T.mor₂)

Tactic:
t.isIso₂_truncGE_map_of_isLE _ hT _ _ rfl h₁

Premises used: CategoryTheory.Triangulated.TStructure.isIso₂_truncGE_map_of_isLE, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
dsimp : t.IsGE ((t.truncLT (b + 1)).obj X) a
⊢ t.IsGE ((t.truncLE b).obj X) a

Tactic:
dsimp [truncLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncLE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ t.IsGE ((t.truncLT (b + 1)).obj X) a

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
dsimp : t.IsLE ((t.truncGE (a + 1)).obj X) b
⊢ t.IsLE ((t.truncGT a).obj X) b

Tactic:
dsimp [truncGT]

Premises used: CategoryTheory.Triangulated.TStructure.truncGT
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ t.IsLE ((t.truncGE (a + 1)).obj X) b

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b : ℤ
dsimp : t.IsLE ((t.truncGE a).obj ((t.truncLE b).obj X)) b
⊢ t.IsLE ((t.truncGELE a b).obj X) b

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b : ℤ
⊢ t.IsLE ((t.truncGE a).obj ((t.truncLE b).obj X)) b

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b : ℤ
h : a ≤ b
X : C
⊢ a + 1 ≤ b + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b : ℤ
h : b ≤ a
X : C
⊢ b + 1 ≤ a + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
⊢ n ≤ 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
this : ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0
rw : f₁ - f₂ = 0
⊢ f₁ = f₂

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
suffices : ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0
⊢ f₁ = f₂

Tactic:
suffices ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0 by rw [← sub_eq_zero]; 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
h₂ : f.hom₁ = TriangleMorphism.hom₁ 0
h₃ : f.hom₂ = TriangleMorphism.hom₂ 0
h₄ : f.hom₃ = TriangleMorphism.hom₃ 0
⊢ f = 0

Tactic:
ext
-- 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₁ ≫ T'.invRotate.mor₂ = 0

Tactic:
simp [← f.comm₁, hf]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
h₂ : ∀ (g : T.obj₁ ⟶ T'.invRotate.obj₁) (hg : f.hom₁ = g ≫ T'.invRotate.mor₁), f.hom₁ = TriangleMorphism.hom₁ 0
⊢ f.hom₁ = TriangleMorphism.hom₁ 0

Tactic:
obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _ hT')
      f.hom₁ (by simp [← f.comm₁, hf])

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.Pretriangulated.TriangleMorphism.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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
g : T.obj₁ ⟶ T'.invRotate.obj₁
hg : f.hom₁ = g ≫ T'.invRotate.mor₁
⊢ a < b + 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
g : T.obj₁ ⟶ T'.invRotate.obj₁
hg : f.hom₁ = g ≫ T'.invRotate.mor₁
⊢ f.hom₁ = TriangleMorphism.hom₁ 0

Tactic:
simp [hg, t.zero_of_isLE_of_isGE g a (b + 1) (by lia)
      h₀ (t.isGE_shift _ b (-1) (b + 1))]

Premises used: CategoryTheory.Triangulated.TStructure.zero_of_isLE_of_isGE, HAdd.hAdd, CategoryTheory.Triangulated.TStructure.isGE_shift, 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₂ = TriangleMorphism.hom₂ 0

Tactic:
simp [hf]
-- 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
h₃ :
  ∀ (g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ T'.obj₃) (hg : f.hom₃ = T.mor₃ ≫ g),
    f.hom₃ = TriangleMorphism.hom₃ 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0

Tactic:
obtain ⟨g, hg⟩ := T.yoneda_exact₃ hT f.hom₃ (by cat_disch)

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃, CategoryTheory.Pretriangulated.TriangleMorphism.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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ T'.obj₃
hg : f.hom₃ = T.mor₃ ≫ g
⊢ a - 1 < b

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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ T'.obj₃
hg : f.hom₃ = T.mor₃ ≫ g
⊢ f.hom₃ = TriangleMorphism.hom₃ 0

Tactic:
simp [hg, t.zero_of_isLE_of_isGE g (a - 1) b (by lia)
      (t.isLE_shift _ a 1 (a - 1)) inferInstance]

Premises used: HSub.hSub, inferInstance, CategoryTheory.Triangulated.TStructure.isLE_shift, CategoryTheory.Triangulated.TStructure.zero_of_isLE_of_isGE, 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
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
φ : T.obj₂ ⟶ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
obtain : ∀ (a : T.obj₁ ⟶ T'.obj₁) (comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁), ∃ (f : T ⟶ T'), f.hom₂ = φ
⊢ ∃ (f : T ⟶ T'), f.hom₂ = φ

Tactic:
obtain ⟨a, comm₁⟩ := T'.coyoneda_exact₂ hT' (T.mor₁ ≫ φ) (t.zero _ a b)

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, CategoryTheory.Triangulated.TStructure.zero, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pretriangulated.Triangle.mor₁
-- 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
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
φ : T.obj₂ ⟶ T'.obj₂
a_1 b : ℤ
h₀ : t.IsLE T.obj₁ a_1
h₁' : t.IsGE T'.obj₃ b
h : a_1 < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
obtain :
  ∀ (c : T.obj₃ ⟶ T'.obj₃) (comm₂ : T.mor₂ ≫ c = φ ≫ T'.mor₂)
    (comm₃ : T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T'.mor₃), ∃ (f : T ⟶ T'), f.hom₂ = φ
⊢ ∃ (f : T ⟶ T'), f.hom₂ = φ

Tactic:
obtain ⟨c, comm₂, comm₃⟩ := complete_distinguished_triangle_morphism _ _ hT hT' a φ comm₁

Premises used: CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism