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
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
i₁ : ℤ
hi₁ : t.IsLE T.obj₁ i₁
i₃ : ℤ
hi₃ : t.IsLE T.obj₃ i₃
⊢ t.minus T.obj₂

Tactic:
⟨max i₁ i₃, t.isLE₂ T hT _ (t.isLE_of_le _ _ _ (le_max_left i₁ i₃))
      (t.isLE_of_le _ _ _ (le_max_right i₁ i₃))⟩

Premises used: le_max_right, CategoryTheory.Triangulated.TStructure.minus, CategoryTheory.Triangulated.TStructure.isLE₂, Max.max, CategoryTheory.Triangulated.TStructure.isLE_of_le, Exists.intro, le_max_left
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
i₁ : ℤ
hi₁ : t.IsLE T.obj₁ i₁
i₃ : ℤ
hi₃ : t.IsLE T.obj₃ i₃
⊢ t.minus T.obj₂

Tactic:
exact ⟨max i₁ i₃, t.isLE₂ T hT _ (t.isLE_of_le _ _ _ (le_max_left i₁ i₃))
      (t.isLE_of_le _ _ _ (le_max_right i₁ i₃))⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
i₁ : ℤ
hi₁ : t.IsGE T.obj₁ i₁
i₃ : ℤ
hi₃ : t.IsGE T.obj₃ i₃
⊢ t.plus T.obj₂

Tactic:
⟨min i₁ i₃, t.isGE₂ T hT _ (t.isGE_of_ge _ _ _ (min_le_left i₁ i₃))
      (t.isGE_of_ge _ _ _ (min_le_right i₁ i₃))⟩

Premises used: CategoryTheory.Triangulated.TStructure.plus, CategoryTheory.Triangulated.TStructure.isGE₂, min_le_left, min_le_right, Exists.intro, Min.min, 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
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
i₁ : ℤ
hi₁ : t.IsGE T.obj₁ i₁
i₃ : ℤ
hi₃ : t.IsGE T.obj₃ i₃
⊢ t.plus T.obj₂

Tactic:
exact ⟨min i₁ i₃, t.isGE₂ T hT _ (t.isGE_of_ge _ _ _ (min_le_left i₁ i₃))
      (t.isGE_of_ge _ _ _ (min_le_right i₁ i₃))⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
⊢ (t.plus ⊓ t.minus).IsTriangulated

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 Y : C
f : X ⟶ Y
n : ℤ
⊢ IsIso ((t.truncLT n).map f) ↔
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
      t.IsGE Z n

Tactic:
⟨fun hf ↦ ?_, fun ⟨Z, g, h, mem, _⟩ ↦ ?_⟩

Premises used: CategoryTheory.IsIso, CategoryTheory.Triangulated.TStructure.truncLT, _private.0.CategoryTheory.Triangulated.TStructure.isIso_truncLT_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
X Y : C
f : X ⟶ Y
n : ℤ
refine_1 :
  ∀ (hf : IsIso ((t.truncLT n).map f)),
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
      t.IsGE Z n
refine_2 :
  (∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
      t.IsGE Z n) →
    ∀ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X))
      (mem :
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
          (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
      t.IsGE Z n → IsIso ((t.truncLT n).map f)
⊢ IsIso ((t.truncLT n).map f) ↔
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
      t.IsGE Z n

Tactic:
refine ⟨fun hf ↦ ?_, fun ⟨Z, g, 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
X Y : C
f : X ⟶ Y
n : ℤ
hf : IsIso ((t.truncLT n).map f)
⊢ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n

Tactic:
⟨(t.truncGE n).obj Y, (t.truncGEπ n).app Y,
      (t.truncGEδLT n).app Y ≫ (inv ((t.truncLT n).map f))⟦1⟧',
      isomorphic_distinguished _ (t.triangleLTGE_distinguished n Y) _ ?_, inferInstance⟩

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.shiftFunctor, inferInstance, CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Functor.map, CategoryTheory.Triangulated.TStructure.truncGEδLT, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, OfNat.ofNat, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, 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 Y : C
f : X ⟶ Y
n : ℤ
hf : IsIso ((t.truncLT n).map f)
refine_1 :
  Triangle.mk ((t.truncLTι n).app X ≫ f) ((t.truncGEπ n).app Y)
      ((t.truncGEδLT n).app Y ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (inv ((t.truncLT n).map f))) ≅
    (t.triangleLTGE n).obj Y
⊢ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n

Tactic:
refine ⟨(t.truncGE n).obj Y, (t.truncGEπ n).app Y,
      (t.truncGEδLT n).app Y ≫ (inv ((t.truncLT n).map f))⟦1⟧',
      isomorphic_distinguished _ (t.triangleLTGE_distinguished n Y) _ ?_, inferInstance⟩
-- 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 Y : C
f : X ⟶ Y
n : ℤ
hf : IsIso ((t.truncLT n).map f)
⊢ Triangle.mk ((t.truncLTι n).app X ≫ f) ((t.truncGEπ n).app Y)
      ((t.truncGEδLT n).app Y ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (inv ((t.truncLT n).map f))) ≅
    (t.triangleLTGE n).obj Y

Tactic:
exact Triangle.isoMk _ _ (asIso ((t.truncLT n).map f)) (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.Triangle.isoMk, 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
dsimp : t.IsLE ((t.truncLT n).obj X) (n - 1)
⊢ t.IsLE (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).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 Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z 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 Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 dsimp : t.IsGE Z n
⊢ t.IsGE (Triangle.mk ((t.truncLTι n).app X ≫ f) g 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
⊢ t.IsGE 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
dsimp : t.IsLE ((t.truncLT n).obj Y) (n - 1)
⊢ t.IsLE ((t.triangleLTGE n).obj Y).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 Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
⊢ t.IsLE ((t.truncLT n).obj Y) (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 Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
refine_2 :
  ∀ (e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y)
    (he : e.hom.hom₂ = Iso.hom (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂)),
    IsIso ((t.truncLT n).map f)
⊢ IsIso ((t.truncLT n).map f)

Tactic:
obtain ⟨e, he⟩ := t.triangle_iso_exists
      mem (t.triangleLTGE_distinguished n Y) (Iso.refl _) (n - 1) n
      (by dsimp; infer_instance) (by dsimp; infer_instance)
      (by dsimp; infer_instance) (by dsimp; infer_instance)

Premises used: CategoryTheory.Triangulated.TStructure.triangle_iso_exists, HSub.hSub, CategoryTheory.Iso.refl, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, 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 Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = Iso.hom (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂)
this : (t.truncLT n).map f = e.hom.hom₁
rw : IsIso e.hom.hom₁
⊢ IsIso ((t.truncLT n).map f)

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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = Iso.hom (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂)
this : (t.truncLT n).map f = 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = Iso.hom (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂)
refine_2 : (t.truncLT n).map f = e.hom.hom₁
⊢ IsIso ((t.truncLT n).map f)

Tactic:
suffices ((t.truncLT n).map f) = 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
X Y : C
f : X ⟶ Y
n : ℤ
h_1 :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)),
    t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app X ≫ f) g h)
h_2 : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = Iso.hom (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂)
⊢ (t.truncLT n).map f = e.hom.hom₁

Tactic:
exact t.to_truncLT_obj_ext (Eq.trans (by cat_disch) e.hom.comm₁)