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
X : C
a b : ℤ
inst_6 : t.IsLE X b
h : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b

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 : ℤ
inst_6 : t.IsLE X b
h : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
exact 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 : ℤ
inst_6 : t.IsLE X b
h : ¬a ≤ b + 1
⊢ a - 1 + 1 = a

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
inst_6 : t.IsLE X b
h : ¬a ≤ b + 1
⊢ b ≤ a - 1

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 : ℤ
inst_6 : t.IsLE X b
h : ¬a ≤ b + 1
⊢ IsIso ((t.truncLTι a).app X)

Tactic:
have := (t.isLE_iff_isIso_truncLTι_app (a - 1) a (by lia) X).1 (t.isLE_of_le _ b _ (by lia))
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
inst_6 : t.IsLE X b
h : ¬a ≤ b + 1
this : IsIso ((t.truncLTι a).app X)
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
t.isLE_of_iso (show X ≅ _ from (asIso ((t.truncLTι a).app X)).symm) _

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.isLE_of_iso, CategoryTheory.Iso.symm, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
inst_6 : t.IsLE X b
h : ¬a ≤ b + 1
this : IsIso ((t.truncLTι a).app X)
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
exact t.isLE_of_iso (show X ≅ _ from (asIso ((t.truncLTι a).app X)).symm) _

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.isLE_of_iso, CategoryTheory.Iso.symm, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
inst_6 : t.IsGE X a
pos : ∀ (h : a ≤ b), t.IsGE ((t.truncGE b).obj X) a
neg : ∀ (h : ¬a ≤ b), t.IsGE ((t.truncGE b).obj X) a
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
by_cases h : a ≤ b
-- 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.IsGE X a
h : a ≤ b
⊢ t.IsGE ((t.truncGE b).obj X) a

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
X : C
a b : ℤ
inst_6 : t.IsGE X a
h : a ≤ b
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
exact 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
X : C
a b : ℤ
inst_6 : t.IsGE X a
h : ¬a ≤ b
⊢ 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 : ℤ
inst_6 : t.IsGE X a
h : ¬a ≤ b
⊢ t.IsGE X b

Tactic:
have : t.IsGE X b := t.isGE_of_ge X b a (by lia)
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
inst_6 : t.IsGE X a
h : ¬a ≤ b
this : t.IsGE X b
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
t.isGE_of_iso (show X ≅ _ from asIso ((t.truncGEπ b).app X)) _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.NatTrans.app, CategoryTheory.asIso, CategoryTheory.Triangulated.TStructure.truncGEπ
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
inst_6 : t.IsGE X a
h : ¬a ≤ b
this : t.IsGE X b
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
exact t.isGE_of_iso (show X ≅ _ from asIso ((t.truncGEπ b).app X)) _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.NatTrans.app, CategoryTheory.asIso, CategoryTheory.Triangulated.TStructure.truncGEπ
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
dsimp : t.IsGE ((t.truncGE a).obj ((t.truncLT b).obj X)) a
⊢ t.IsGE ((t.truncGELT a b).obj X) a

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
⊢ t.IsGE ((t.truncGE a).obj ((t.truncLT b).obj X)) a

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
dsimp : t.IsLE ((t.truncLT b).obj ((t.truncGE a).obj X)) (b - 1)
⊢ t.IsLE ((t.truncLTGE a b).obj X) (b - 1)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
a b : ℤ
⊢ t.IsLE ((t.truncLT b).obj ((t.truncGE a).obj X)) (b - 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
rw :
  ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n
⊢ IsIso ((t.truncLT n).map T.mor₁)

Tactic:
rw [isIso_truncLT_map_iff]

Premises used: CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_iff
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
obtain :
  ∀ (Z : C) (g : T.obj₂ ⟶ Z) (k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)),
    ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
      (_ :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
      t.IsGE Z n
⊢ ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n

Tactic:
obtain ⟨Z, g, k, mem⟩ := distinguished_cocone_triangle ((t.truncLTι n).app T.obj₁ ≫ T.mor₁)

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pretriangulated.Triangle.mor₁, 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
⊢ ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n

Tactic:
⟨_, _, _, mem, ?_⟩

Premises used: Exists.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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
refine : t.IsGE Z n
⊢ ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n

Tactic:
refine ⟨_, _, _, mem, ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
dsimp : t.IsGE ((t.truncGE n).obj T.obj₁) n
⊢ t.IsGE (Triangle.mk H.m₁ H.m₃ (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncGEπ n).app T.obj₁))).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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE ((t.truncGE n).obj T.obj₁) 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
dsimp : t.IsGE T.obj₃ n
⊢ t.IsGE (Triangle.mk H.m₁ H.m₃ (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncGEπ n).app T.obj₁))).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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE T.obj₃ 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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE Z n

Tactic:
exact t.isGE₂ _ H.mem n (by dsimp; infer_instance) (by dsimp; infer_instance)

Premises used: CategoryTheory.Triangulated.Octahedron.mem, CategoryTheory.Triangulated.TStructure.isGE₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
rw :
  ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_
    :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
    t.IsLE X n₀
⊢ IsIso ((t.truncGE n₁).map T.mor₂)

Tactic:
rw [isIso_truncGE_map_iff _ _ _ _ h]

Premises used: CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
obtain :
  ∀ (X : C) (f : X ⟶ T.obj₂) (k : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k)),
    ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
      (_ :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
      t.IsLE X n₀
⊢ ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_
    :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
    t.IsLE X n₀

Tactic:
obtain ⟨X, f, k, mem⟩ := distinguished_cocone_triangle₁ (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃)

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

Tactic:
⟨_, _, _, mem, ?_⟩

Premises used: Exists.intro