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 x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2 + (TruncAux.triangleFunctor t n).map x_3) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))

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 x_1 : C
x_2 x_3 : x ⟶ x_1
dsimp :
  Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))
⊢ (t.truncGE n).map (x_2 + x_3) = (t.truncGE n).map x_2 + (t.truncGE n).map x_3

Tactic:
dsimp only [truncGE, Functor.comp_map]

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Functor.comp_map
-- 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 x_1 : C
x_2 x_3 : x ⟶ x_1
rw :
  Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2 + (TruncAux.triangleFunctor t n).map x_3) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))
⊢ Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))

Tactic:
rw [Functor.map_add]

Premises used: CategoryTheory.Functor.map_add
-- 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 x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2 + (TruncAux.triangleFunctor t n).map x_3) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))

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 Y : C
f : X ⟶ Y
⊢ (t.truncGEπ n).app X ≫ (t.truncGE n).map f = f ≫ (t.truncGEπ n).app Y

Tactic:
((t.truncGEπ n).naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm, 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
a b : ℤ
hn : a ≤ b + 1
dsimp : t.IsLE (TruncAux.triangle t a X).obj₁ (a - 1)
⊢ t.IsLE ((t.truncLT a).obj X) (a - 1)

Tactic:
dsimp [truncLT]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT
-- 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
a b : ℤ
hn : a ≤ b + 1
⊢ t.IsLE (TruncAux.triangle t a X).obj₁ (a - 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
X : C
a b : ℤ
hn : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) (a - 1)

Tactic:
have : t.IsLE ((t.truncLT a).obj X) (a - 1) := by dsimp [truncLT]; 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
X : C
a b : ℤ
hn : a ≤ b + 1
this : t.IsLE ((t.truncLT a).obj X) (a - 1)
⊢ 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
X : C
a b : ℤ
hn : a ≤ b + 1
this : t.IsLE ((t.truncLT a).obj X) (a - 1)
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
exact t.isLE_of_le _ (a - 1) _ (by lia)

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isLE_of_le, 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
X : C
n : ℤ
⊢ t.IsLE ((t.truncLT n).obj X) (n - 1)

Tactic:
t.isLE_truncLT_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isLE_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
X : C
n : ℤ
⊢ t.IsLE ((t.truncLT (n + 1)).obj X) n

Tactic:
t.isLE_truncLT_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isLE_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
X : C
a b : ℤ
hn : b ≤ a
dsimp : t.IsGE (TruncAux.triangle t a X).obj₃ a
⊢ t.IsGE ((t.truncGE a).obj X) a

Tactic:
dsimp [truncGE]

Premises used: 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
a b : ℤ
hn : b ≤ a
⊢ t.IsGE (TruncAux.triangle t a X).obj₃ 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
X : C
a b : ℤ
hn : b ≤ a
⊢ t.IsGE ((t.truncGE a).obj X) a

Tactic:
have : t.IsGE ((t.truncGE a).obj X) a := by dsimp [truncGE]; 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
X : C
a b : ℤ
hn : b ≤ a
this : t.IsGE ((t.truncGE a).obj X) a
⊢ b ≤ 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
X : C
a b : ℤ
hn : b ≤ a
this : t.IsGE ((t.truncGE a).obj X) a
⊢ t.IsGE ((t.truncGE a).obj X) b

Tactic:
exact t.isGE_of_ge _ _ a (by lia)

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_ge
-- 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 : ℤ
⊢ t.IsGE ((t.truncGE n).obj X) n

Tactic:
t.isGE_truncGE_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isGE_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 : ℤ
X : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLTGE n).obj X)

Tactic:
TruncAux.triangleFunctor_obj_distinguished t n X

Premises used: Set.Mem, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, Classical.choose, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_obj_distinguished
-- 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 : ℤ
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
X : C
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
X : C
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
X : C
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
⊢ (t.truncLTι n).app X ≫ (t.truncGEπ n).app X = 0

Tactic:
comp_distTriang_mor_zero₁₂ _ (t.triangleLTGE_distinguished n X)

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Classical.choose
-- 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
⊢ (t.truncGEπ n).app X ≫ (t.truncGEδLT n).app X = 0

Tactic:
comp_distTriang_mor_zero₂₃ _ (t.triangleLTGE_distinguished n X)

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Classical.choose
-- 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
⊢ (t.truncGEδLT n).app X ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLTι n).app X) = 0

Tactic:
comp_distTriang_mor_zero₃₁ _ (t.triangleLTGE_distinguished n X)

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Classical.choose
-- 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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.natTransTruncLTOfLE a b h).app X ≫ (t.truncLTι b).app X = (t.truncLTι a).app X

Tactic:
simpa using ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₁.symm

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, Eq.symm, CategoryTheory.NatTrans.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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.truncGEπ a).app X ≫ (t.natTransTruncGEOfLE a b h).app X = (t.truncGEπ b).app X

Tactic:
simpa only [TruncAux.triangleFunctor_obj, TruncAux.triangle_obj₂,
    TruncAux.triangleFunctorNatTransOfLE_app_hom₂, Category.id_comp] using
    ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₂

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_app_hom₂, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_obj₂, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_obj, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- 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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.truncGEδLT a).app X ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.natTransTruncLTOfLE a b h).app X) =
    (t.natTransTruncGEOfLE a b h).app X ≫ (t.truncGEδLT b).app X

Tactic:
((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₃

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, Classical.choose, CategoryTheory.NatTrans.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
a b : ℤ
h : a ≤ b
w :
  ∀ (X : C),
    (t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C (A := ℤ) 1)).app X =
      (t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b).app X
⊢ t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C (A := ℤ) 1) =
    t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b

Tactic:
ext X
-- 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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C (A := ℤ) 1)).app X =
    (t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b).app X

Tactic:
t.truncGEδLT_comp_natTransTruncLTOfLE_app a b h X

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C (A := ℤ) 1)).app X =
    (t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b).app X

Tactic:
exact t.truncGEδLT_comp_natTransTruncLTOfLE_app a b h X

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_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
a b : ℤ
h : a ≤ b
⊢ t.truncLTι a ≫ 𝟙 (𝟭 C) = t.natTransTruncLTOfLE a b h ≫ t.truncLTι b

Tactic:
simp
-- 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
a b : ℤ
h : a ≤ b
⊢ t.truncGEπ a ≫ t.natTransTruncGEOfLE a b h = 𝟙 (𝟭 C) ≫ t.truncGEπ b

Tactic:
simp
-- 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
a : ℤ
⊢ a ≤ a

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
a : ℤ
⊢ t.natTransTriangleLTGEOfLE a a ⋯ = 𝟙 (t.triangleLTGE a)

Tactic:
TruncAux.triangleFunctorNatTransOfLE_refl t a

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap, CategoryTheory.Pretriangulated.Triangle.functorHomMk', CategoryTheory.Pretriangulated.Triangle.functorHomMk, CategoryTheory.Triangulated.TStructure.triangleLTGE, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE, CategoryTheory.Pretriangulated.Triangle.functorMk, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE, Classical.choose, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_refl, CategoryTheory.Pretriangulated.Triangle.mk