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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k)
refine : t.IsLE X n₀
⊢ ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_
    :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
    t.IsLE X n₀

Tactic:
refine ⟨_, _, _, mem, ?_⟩
-- 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k)
subst :
  ∀ (k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)),
    t.IsLE X n₀
⊢ t.IsLE X n₀

Tactic:
subst h
-- 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
have : ∀ (H : Octahedron ⋯ ⋯ ⋯ ⋯), t.IsLE X n₀
⊢ t.IsLE X n₀

Tactic:
have H := someOctahedron rfl (rot_of_distTriang _ hT)
    (rot_of_distTriang _ (t.triangleLTGE_distinguished (n₀ + 1) T.obj₃))
    (rot_of_distTriang _ mem)
-- 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
H : Octahedron ⋯ ⋯ ⋯ ⋯
⊢ 1 + (n₀ - 1) = 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
H : Octahedron ⋯ ⋯ ⋯ ⋯
⊢ t.IsLE (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (n₀ - 1)

Tactic:
have : t.IsLE (X⟦(1 : ℤ)⟧) (n₀ - 1) :=
    t.isLE₂ _ H.mem (n₀ - 1) (t.isLE_shift T.obj₁ n₀ 1 (n₀ - 1) (by lia))
      (t.isLE_shift ((t.truncLT (n₀ + 1)).obj T.obj₃) n₀ 1 (n₀-1) (by 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
H : Octahedron ⋯ ⋯ ⋯ ⋯
this : t.IsLE (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (n₀ - 1)
⊢ 1 + (n₀ - 1) = 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
H : Octahedron ⋯ ⋯ ⋯ ⋯
this : t.IsLE (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (n₀ - 1)
⊢ t.IsLE X n₀

Tactic:
exact t.isLE_of_shift X n₀ 1 (n₀ - 1) (by lia)

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isLE_of_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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
rw : IsZero.{v, u} ((t.truncLT a).obj ((t.truncLT b).obj X))
⊢ t.IsGE ((t.truncLT b).obj X) a

Tactic:
rw [t.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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
dsimp : t.IsGE ((t.truncGE b).obj X) a
⊢ t.IsGE ((t.triangleLTGE b).obj X).obj₃ a

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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ t.IsGE ((t.truncGE b).obj X) a

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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ IsIso ((t.truncLT a).map ((t.triangleLTGE b).obj X).mor₁)

Tactic:
have := t.isIso₁_truncLT_map_of_isGE _ ((t.triangleLTGE_distinguished b X)) a
    (by dsimp; 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ IsZero.{v, u} ((t.truncLT a).obj ((t.truncLT b).obj X))

Tactic:
IsZero.of_iso ?_ (asIso ((t.truncLT a).map ((t.truncLTι b).app X)))

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Functor.map, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
refine : IsZero.{v, u} ((t.truncLT a).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))
⊢ IsZero.{v, u} ((t.truncLT a).obj ((t.truncLT b).obj X))

Tactic:
refine IsZero.of_iso ?_ (asIso ((t.truncLT a).map ((t.truncLTι b).app X)))

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Functor.map, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
rwa rwa₁ rwa₂ rwa₃ : t.IsGE (Functor.obj.{v, v, u, u} (𝟭 C) X) a
⊢ IsZero.{v, u} ((t.truncLT a).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))

Tactic:
rwa [← 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
rw : IsZero.{v, u} ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))
⊢ t.IsLE ((t.truncGE a).obj X) b

Tactic:
rw [t.isLE_iff_isZero_truncGE_obj b (b + 1) rfl]

Premises used: CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj, HAdd.hAdd, OfNat.ofNat, rfl
-- 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
dsimp : t.IsLE ((t.truncLT a).obj X) b
⊢ t.IsLE ((t.triangleLTGE a).obj X).obj₁ b

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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ t.IsLE ((t.truncLT a).obj X) b

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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ IsIso ((t.truncGE (b + 1)).map ((t.triangleLTGE a).obj X).mor₂)

Tactic:
have := t.isIso₂_truncGE_map_of_isLE _ (t.triangleLTGE_distinguished a X) b _ rfl
    (by dsimp; 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
this : IsIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))
⊢ IsZero.{v, u} ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))

Tactic:
IsZero.of_iso ?_ (asIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))).symm

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Functor.map, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, CategoryTheory.Iso.symm, OfNat.ofNat, 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
this : IsIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))
refine : IsZero.{v, u} ((t.truncGE (b + 1)).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))
⊢ IsZero.{v, u} ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))

Tactic:
refine IsZero.of_iso ?_ (asIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))).symm

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Functor.map, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, CategoryTheory.Iso.symm, OfNat.ofNat, 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
this : IsIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))
rwa rwa₁ rwa₂ rwa₃ : t.IsLE (Functor.obj.{v, v, u, u} (𝟭 C) X) b
⊢ IsZero.{v, u} ((t.truncGE (b + 1)).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))

Tactic:
rwa [← isLE_iff_isZero_truncGE_obj _ _ _ rfl]

Premises used: CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj, rfl
-- 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
dsimp : t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 1)
⊢ t.IsLE ((t.truncGELT a b).obj X) (b - 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
⊢ t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
dsimp : t.IsGE ((t.truncLT b).obj ((t.truncGE a).obj X)) a
⊢ t.IsGE ((t.truncLTGE a b).obj X) a

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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
⊢ t.IsGE ((t.truncLT b).obj ((t.truncGE a).obj X)) a

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : b ≤ a
X : C
⊢ a - 1 + 1 = a

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : b ≤ a
X : C
⊢ b ≤ a - 1 + 1

Tactic:
simpa
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
⊢ a ≤ 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
inst_6 : IsTriangulated.{v, u} C
X : C
n : ℤ
⊢ n ≤ n

Tactic:
rfl
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ b - 1 + 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
rw : t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 1)
⊢ IsIso (X := (t.truncLT b).obj ((t.truncGE a).obj ((t.truncLT b).obj X)))
    ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))

Tactic:
rw [← t.isLE_iff_isIso_truncLTι_app (b - 1) b (by lia)]

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app, 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
x x_1 : C
x_2 : x ⟶ x_1
dsimp :
  ((t.truncGE a).map ((t.truncLT b).map x_2) ≫
        t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x_1 ≫ (t.truncGEπ a).app x_1) a) (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1) =
    (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x ≫ (t.truncGEπ a).app x) a) (b - 1) b ⋯ ≫
        (t.truncLT b).map ((t.truncGE a).map x_2)) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1)
⊢ ((t.truncGELT a b).map x_2 ≫
        t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x_1 ≫ (t.truncGEπ a).app x_1) a) (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1) =
    (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x ≫ (t.truncGEπ a).app x) a) (b - 1) b ⋯ ≫
        (t.truncLTGE a b).map x_2) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
x x_1 : C
x_2 : x ⟶ x_1
⊢ (t.truncGEπ a).app ((t.truncLT b).obj x) ≫
      ((t.truncGE a).map ((t.truncLT b).map x_2) ≫
          t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x_1 ≫ (t.truncGEπ a).app x_1) a) (b - 1) b ⋯) ≫
        (t.truncLTι b).app ((t.truncGE a).obj x_1) =
    (t.truncGEπ a).app ((t.truncLT b).obj x) ≫
      (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x ≫ (t.truncGEπ a).app x) a) (b - 1) b ⋯ ≫
          (t.truncLT b).map ((t.truncGE a).map x_2)) ≫
        (t.truncLTι b).app ((t.truncGE a).obj x_1)

Tactic:
simp