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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
⊢ IsIso ((t.truncGE n₁).map g) ↔
    ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
      t.IsLE X n₀

Tactic:
⟨fun hf ↦ ?_, fun ⟨X, f, h, mem, _⟩ ↦ ?_⟩

Premises used: CategoryTheory.IsIso, CategoryTheory.Triangulated.TStructure.truncGE, _private.0.CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff.match_1, CategoryTheory.Functor.map, Iff.intro
-- 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
refine_1 :
  ∀ (hf : IsIso ((t.truncGE n₁).map g)),
    ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
      t.IsLE X n₀
refine_2 :
  (∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
      t.IsLE X n₀) →
    ∀ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
      t.IsLE X n₀ → IsIso ((t.truncGE n₁).map g)
⊢ IsIso ((t.truncGE n₁).map g) ↔
    ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
      t.IsLE X n₀

Tactic:
refine ⟨fun hf ↦ ?_, fun ⟨X, f, h, 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
subst : ∀ (hf : IsIso ((t.truncGE (n₀ + 1)).map g)), t.IsLE ((t.truncLT (n₀ + 1)).obj Y) n₀
⊢ t.IsLE ((t.truncLT n₁).obj Y) n₀

Tactic:
subst hn
-- 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
Y Z : C
g : Y ⟶ Z
n₀ : ℤ
hf : IsIso ((t.truncGE (n₀ + 1)).map g)
⊢ t.IsLE ((t.truncLT (n₀ + 1)).obj Y) 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
refine_1 :
  Triangle.mk ((t.truncLTι n₁).app Y) (g ≫ (t.truncGEπ n₁).app Z)
      (inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y) ≅
    (t.triangleLTGE n₁).obj Y
⊢ ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀

Tactic:
refine ⟨_, (t.truncLTι n₁).app Y, inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y,
      isomorphic_distinguished _ (t.triangleLTGE_distinguished n₁ Y) _ ?_,
      by subst hn; 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ ((t.triangleLTGE n₁).obj Y).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂) =
    Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₁) ≫
      (Triangle.mk ((t.truncLTι n₁).app Y) (g ≫ (t.truncGEπ n₁).app Z)
          (inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y)).mor₁

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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ ((t.triangleLTGE n₁).obj Y).mor₂ ≫ (asIso ((t.truncGE n₁).map g)).hom =
    Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂) ≫
      (Triangle.mk ((t.truncLTι n₁).app Y) (g ≫ (t.truncGEπ n₁).app Z)
          (inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y)).mor₂

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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ ((t.triangleLTGE n₁).obj Y).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₁)) =
    (asIso ((t.truncGE n₁).map g)).hom ≫
      (Triangle.mk ((t.truncLTι n₁).app Y) (g ≫ (t.truncGEπ n₁).app Z)
          (inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y)).mor₃

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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ Triangle.mk ((t.truncLTι n₁).app Y) (g ≫ (t.truncGEπ n₁).app Z)
      (inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y) ≅
    (t.triangleLTGE n₁).obj Y

Tactic:
exact Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
      (asIso ((t.truncGE n₁).map g)) (by simp) (by simp) (by simp))

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Iso.symm, 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
dsimp : t.IsLE ((t.truncLT n₁).obj Y) n₀
⊢ t.IsLE ((t.triangleLTGE n₁).obj Y).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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
rw : t.IsLE ((t.truncLT (n₀ + 1)).obj Y) n₀
⊢ t.IsLE ((t.truncLT n₁).obj Y) n₀

Tactic:
rw [← hn]
-- 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsLE ((t.truncLT (n₀ + 1)).obj Y) 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
dsimp : t.IsGE ((t.truncGE n₁).obj Y) n₁
⊢ t.IsGE ((t.triangleLTGE n₁).obj Y).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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsGE ((t.truncGE n₁).obj Y) 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 dsimp : t.IsLE X n₀
⊢ t.IsLE (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h).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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsLE 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
dsimp : t.IsGE ((t.truncGE n₁).obj Z) n₁
⊢ t.IsGE (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h).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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsGE ((t.truncGE n₁).obj Z) 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
refine_2 :
  ∀ (e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
    (he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)), IsIso ((t.truncGE n₁).map g)
⊢ IsIso ((t.truncGE n₁).map g)

Tactic:
obtain ⟨e, he⟩ :=
      t.triangle_iso_exists (t.triangleLTGE_distinguished n₁ Y) mem (Iso.refl _) n₀ n₁
        (by dsimp; rw [← hn]; infer_instance) (by dsimp; infer_instance)
        (by dsimp; infer_instance) (by dsimp; infer_instance)

Premises used: CategoryTheory.Triangulated.TStructure.triangle_iso_exists, CategoryTheory.Iso.refl, CategoryTheory.Triangulated.TStructure.triangleLTGE_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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)
this : (t.truncGE n₁).map g = e.hom.hom₃
rw : IsIso e.hom.hom₃
⊢ IsIso ((t.truncGE n₁).map g)

Tactic:
rw [this]
-- 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)
this : (t.truncGE n₁).map g = e.hom.hom₃
⊢ IsIso e.hom.hom₃

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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)
refine_2 : (t.truncGE n₁).map g = e.hom.hom₃
⊢ IsIso ((t.truncGE n₁).map g)

Tactic:
suffices ((t.truncGE n₁).map g) = e.hom.hom₃ by rw [this]; 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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ 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 (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)
⊢ (t.truncGE n₁).map g = e.hom.hom₃

Tactic:
exact t.from_truncGE_obj_ext (Eq.trans (by cat_disch) e.hom.comm₂.symm)
-- 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 : ℤ
inst_6 : t.IsLE X b
pos : ∀ (h : a ≤ b + 1), t.IsLE ((t.truncLT a).obj X) b
neg : ∀ (h : ¬a ≤ b + 1), t.IsLE ((t.truncLT a).obj X) b
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
by_cases h : a ≤ b + 1