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
a b : ℤ
h : a + 1 = b
x : C
⊢ ((t.truncGEδLT b).app x ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLEIsoTruncLT a b h).inv.app x)) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLEIsoTruncLT a b h).hom.app x) =
    𝟙 ((t.truncGE b).obj x) ≫ (t.truncGEδLT b).app x

Tactic:
simp only [Category.assoc, Category.id_comp, ← Functor.map_comp,
      Iso.inv_hom_id_app, Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- 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
a b : ℤ
h : a + 1 = b
X : C
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLEGE a b h).obj X)

Tactic:
isomorphic_distinguished _ (t.triangleLTGE_distinguished b X) _
    ((t.triangleLEGEIsoTriangleLTGE a b h).app X)

Premises used: CategoryTheory.Triangulated.TStructure.triangleLEGEIsoTriangleLTGE, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Iso.app
-- 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
n : ℤ
⊢ n + 1 = n + 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
a b : ℤ
h : a + 1 = b
w :
  ∀ (x : C),
    ((t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
            Functor.whiskerRight (Iso.hom (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁))) (shiftFunctor C (A := ℤ) 1)).app
        x =
      ((t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁).app x
⊢ (t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (Iso.hom (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁))) (shiftFunctor C (A := ℤ) 1) =
    (t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁

Tactic:
ext
-- 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
a b : ℤ
h : a + 1 = b
x : C
w :
  ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
    (t.truncGTIsoTruncGE a b h).hom.app x ≫ (t.truncGEδLE a b h).app x
⊢ ((t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (Iso.hom (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁))) (shiftFunctor C (A := ℤ) 1)).app
      x =
    ((t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁).app x

Tactic:
dsimp [truncGTδLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGTδLE
-- 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
a b : ℤ
h : a + 1 = b
x : C
w :
  ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
    (t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x
⊢ ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
    (t.truncGTIsoTruncGE a b h).hom.app x ≫ (t.truncGEδLE a b h).app x

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
a : ℤ
x : C
⊢ ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
    (t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x

Tactic:
simp only [Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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
n : ℤ
X : C
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLEGT n).obj X)

Tactic:
isomorphic_distinguished _ (t.triangleLEGE_distinguished n (n + 1) rfl X) _
    ((t.triangleLEGTIsoTriangleLEGE n (n + 1) rfl).app X)

Premises used: CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished, HAdd.hAdd, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.triangleLEGTIsoTriangleLEGE, CategoryTheory.Iso.app, OfNat.ofNat, 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
n : ℤ
X : C
⊢ t.IsLE X n ↔ IsIso ((t.truncLEι n).app X)

Tactic:
t.isLE_iff_isIso_truncLTι_app n (n + 1) rfl X

Premises used: HAdd.hAdd, CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app, OfNat.ofNat, 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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
rw : IsIso ((t.truncGEπ n₁).app X) ↔ IsIso ((t.truncGTπ n₀).app X)
⊢ t.IsGE X n₁ ↔ IsIso ((t.truncGTπ n₀).app X)

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

Premises used: CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsIso ((t.truncGTπ n₀).app X)

Tactic:
(MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (Arrow.isoMk (Iso.refl _) ((t.truncGTIsoTruncGE _ _ hn₁).symm.app X))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Triangulated.TStructure.truncGTIsoTruncGE, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk
-- 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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsIso ((t.truncGTπ n₀).app X)

Tactic:
exact (MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (Arrow.isoMk (Iso.refl _) ((t.truncGTIsoTruncGE _ _ hn₁).symm.app X))
-- 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
n : ℤ
inst_6 rw : t.IsLE X n
⊢ IsIso ((t.truncLEι n).app X)

Tactic:
rw [← isLE_iff_isIso_truncLEι_app]

Premises used: CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLEι_app
-- 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
n : ℤ
inst_6 : t.IsLE X n
⊢ t.IsLE X n

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
n : ℤ
X : C
rw : IsIso ((t.truncLEι n).app X) ↔ IsZero.{v_1, u_1} ((t.truncGT n).obj X)
⊢ t.IsLE X n ↔ IsZero.{v_1, u_1} ((t.truncGT n).obj X)

Tactic:
rw [t.isLE_iff_isIso_truncLEι_app n X]

Premises used: CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLEι_app
-- 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
n : ℤ
X : C
⊢ IsIso ((t.truncLEι n).app X) ↔ IsZero.{v_1, u_1} ((t.truncGT n).obj X)

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

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁, CategoryTheory.Triangulated.TStructure.triangleLEGT_distinguished, Iff.symm
-- 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
n : ℤ
X : C
⊢ IsIso ((t.truncLEι n).app X) ↔ IsZero.{v_1, u_1} ((t.truncGT n).obj X)

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

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁, CategoryTheory.Triangulated.TStructure.triangleLEGT_distinguished, Iff.symm
-- 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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
rw : IsIso ((t.truncGEπ n₁).app X) ↔ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)
⊢ t.IsGE X n₁ ↔ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)

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

Premises used: CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)

Tactic:
(Triangle.isZero₁_iff_isIso₂ _ (t.triangleLEGE_distinguished n₀ n₁ h X)).symm

Premises used: CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished, Iff.symm, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- 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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)

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

Premises used: CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished, Iff.symm, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- 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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
inst_6 rw : t.IsGE X n₁
⊢ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)

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

Premises used: CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLE_obj
-- 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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
inst_6 : t.IsGE X n₁
⊢ t.IsGE X n₁

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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
⊢ t.IsLE Y (n + 1 - 1)

Tactic:
simpa
-- 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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
⊢ t.IsLE Y (n + 1 - 1)

Tactic:
have : t.IsLE Y (n + 1 - 1) := by simpa
-- 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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
rw : f₁ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X = f₂ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X
⊢ f₁ = f₂

Tactic:
rw [← cancel_mono ((t.truncLEIsoTruncLT n (n + 1) rfl).hom.app _)]

Premises used: CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT, CategoryTheory.cancel_mono, HAdd.hAdd, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, 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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
⊢ (f₁ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X) ≫ NatTrans.app (t.truncLTι (n + 1)) X =
    (f₂ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X) ≫ NatTrans.app (t.truncLTι (n + 1)) X

Tactic:
simpa
-- 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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
⊢ f₁ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X = f₂ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X

Tactic:
exact t.to_truncLT_obj_ext (by simpa)

Premises used: CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext
-- 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
n : ℤ
inst_6 : t.IsLE X n
⊢ n < n + 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
X Y : C
f : X ⟶ Y
n : ℤ
inst_6 : t.IsLE X n
dsimp : t.IsGE ((t.truncGT n).obj Y) (n + 1)
⊢ t.IsGE ((t.triangleLEGT n).obj Y).obj₃ (n + 1)

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 Y : C
f : X ⟶ Y
n : ℤ
inst_6 : t.IsLE X n
⊢ t.IsGE ((t.truncGT n).obj Y) (n + 1)

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 Y : C
f : X ⟶ Y
n : ℤ
inst_6 : t.IsLE X n
⊢ t.liftTruncLE f n ≫ (t.truncLEι n).app Y = f

Tactic:
(t.liftTruncLE_aux f n).choose_spec.symm

Premises used: Exists.choose_spec, CategoryTheory.Triangulated.TStructure.liftTruncLE_aux, CategoryTheory.Triangulated.TStructure.liftTruncLE, Eq.symm
-- 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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst_6 : t.IsGE Y n₁
⊢ n₀ < n₁

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
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst_6 : t.IsGE Y n₁
dsimp : t.IsLE ((t.truncLE n₀).obj X) n₀
⊢ t.IsLE ((t.triangleLEGT n₀).obj X).obj₁ n₀

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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst_6 : t.IsGE Y n₁
⊢ t.IsLE ((t.truncLE n₀).obj X) n₀

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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst_6 : t.IsGE Y n₁
⊢ (t.truncGTπ n₀).app X ≫ t.descTruncGT f n₀ n₁ h = f

Tactic:
(t.descTruncGT_aux f n₀ n₁ h).choose_spec.symm

Premises used: Exists.choose_spec, CategoryTheory.Triangulated.TStructure.descTruncGT, CategoryTheory.Triangulated.TStructure.descTruncGT_aux, Eq.symm
-- 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 b : ℤ
h : a + 1 = b
subst :
  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)
⊢ 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 b

Tactic:
subst h