awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i j : EInt
f : i ⟶ j
X : C
rw :
  (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj j).obj X)
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (homOfLE ⋯)).app ((t.eTruncLT.obj j).obj X)

Tactic:
rw [show homOfLE le_top = f ≫ homOfLE le_top by rfl]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : EInt
X : C
f : i ⟶ ⊥
⊢ Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊥).obj X) ⟶ (t.eTruncLT.obj ⊥).obj X)
    ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
    (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj ⊥).obj X))

Tactic:
simp [truncLT_map_truncLTι_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : EInt
X : C
a : ℤ
f : i ⟶ WithBotTop.coe a
⊢ Eq (α :=
    (t.eTruncLT.obj i).obj ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) ⟶ (t.eTruncLT.obj (WithBotTop.coe a)).obj X)
    ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
    (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X))

Tactic:
simp [truncLT_map_truncLTι_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : EInt
X : C
f : i ⟶ ⊤
⊢ Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊤).obj X) ⟶ (t.eTruncLT.obj ⊤).obj X)
    ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
    (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj ⊤).obj X))

Tactic:
simp [truncLT_map_truncLTι_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i j : EInt
f : i ⟶ j
X : C
bot :
  ∀ (f : i ⟶ ⊥),
    Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊥).obj X) ⟶ (t.eTruncLT.obj ⊥).obj X)
      ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
      (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj ⊥).obj X))
coe :
  ∀ (a : ℤ) (f : i ⟶ WithBotTop.coe a),
    Eq (α :=
      (t.eTruncLT.obj i).obj ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) ⟶ (t.eTruncLT.obj (WithBotTop.coe a)).obj X)
      ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
      (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X))
top :
  ∀ (f : i ⟶ ⊤),
    Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊤).obj X) ⟶ (t.eTruncLT.obj ⊤).obj X)
      ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
      (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj ⊤).obj X))
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj j).obj X)

Tactic:
induction j using WithBotTop.rec with simp [truncLT_map_truncLTι_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
bot : IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊥).obj X)

Tactic:
rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)]

Premises used: CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
bot : IsIso.{v_1, u_1} (𝟙 X)
⊢ IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
⊢ IsIso.{v_1, u_1} (𝟙 X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 : ℤ
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj (WithBotTop.coe n)).obj X)

Tactic:
t.triangleLTGE_distinguished n X

Premises used: Set.Mem, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 : ℤ
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj (WithBotTop.coe n)).obj X)

Tactic:
exact t.triangleLTGE_distinguished n X

Premises used: CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
top : IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊤).obj X)

Tactic:
rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)]

Premises used: CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₃
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
top : IsIso.{v_1, u_1} (𝟙 X)
⊢ IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : EInt
X : C
bot :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊥).obj X)
coe :
  ∀ (n : ℤ),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      ((t.eTriangleLTGE.obj (WithBotTop.coe n)).obj X)
top :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊤).obj X)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj i).obj X)

Tactic:
induction i using WithBotTop.rec with
  | bot =>
    rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
  | coe n => exact t.triangleLTGE_distinguished n X
  | top =>
    rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)]
    dsimp
    infer_instance

Premises used: CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₃, CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 ((t.eTruncLT.obj ⊥).obj X) n

Tactic:
exact isLE_of_isZero _ (by simp) _

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
a : ℤ
coe : t.IsLE ((t.truncLT a).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
a : ℤ
⊢ t.IsLE ((t.truncLT a).obj X) n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 top : t.IsLE X n
⊢ t.IsLE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.ETrunc
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
i : EInt
bot : t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
coe : ∀ (a : ℤ), t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
top : t.IsLE ((t.eTruncLT.obj ⊤).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with
  | bot => exact isLE_of_isZero _ (by simp) _
  | coe _ => dsimp; infer_instance
  | top => dsimp; infer_instance

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 bot : t.IsGE X n
⊢ t.IsGE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.IsGE X n
⊢ t.IsGE X n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.IsGE X n
a : ℤ
coe : t.IsGE ((t.truncGE a).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.IsGE X n
a : ℤ
⊢ t.IsGE ((t.truncGE a).obj X) n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.IsGE X n
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊤).obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.IsGE X n
⊢ t.IsGE ((t.eTruncGE.obj ⊤).obj X) n

Tactic:
exact isGE_of_isZero _ (by simp) _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.IsGE X n
i : EInt
bot : t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
coe : ∀ (a : ℤ), t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n
top : t.IsGE ((t.eTruncGE.obj ⊤).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with
  | bot => dsimp; infer_instance
  | coe _ => dsimp; infer_instance
  | top => exact isGE_of_isZero _ (by simp) _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
h : WithBotTop.coe n ≤ ⊥
⊢ t.IsGE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : ℤ
h : WithBotTop.coe n ≤ WithBotTop.coe i
coe : t.IsGE ((t.truncGE i).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe i)).obj X) n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : ℤ
h : WithBotTop.coe n ≤ WithBotTop.coe i
⊢ n ≤ i

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : ℤ
h : WithBotTop.coe n ≤ WithBotTop.coe i
⊢ t.IsGE ((t.truncGE i).obj X) n

Tactic:
exact t.isGE_of_ge _ _ _ (by simpa using h)

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_ge
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
h : WithBotTop.coe n ≤ ⊤
⊢ t.IsGE ((t.eTruncGE.obj ⊤).obj X) n

Tactic:
t.isGE_of_isZero (Functor.zero_obj _) _

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.isGE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
h : WithBotTop.coe n ≤ ⊤
⊢ t.IsGE ((t.eTruncGE.obj ⊤).obj X) n

Tactic:
exact t.isGE_of_isZero (Functor.zero_obj _) _

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.isGE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
bot : ∀ (h : WithBotTop.coe n ≤ ⊥), t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
coe : ∀ (i : ℤ) (h : WithBotTop.coe n ≤ WithBotTop.coe i), t.IsGE ((t.eTruncGE.obj (WithBotTop.coe i)).obj X) n
top : ∀ (h : WithBotTop.coe n ≤ ⊤), t.IsGE ((t.eTruncGE.obj ⊤).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with
  | bot => simp at h
  | coe i =>
    dsimp
    exact t.isGE_of_ge _ _ _ (by simpa using h)
  | top => exact t.isGE_of_isZero (Functor.zero_obj _) _

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.isGE_of_isZero, CategoryTheory.Triangulated.TStructure.isGE_of_ge
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
h : ⊥ ≤ WithBotTop.coe (n + 1)
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
h : ⊥ ≤ WithBotTop.coe (n + 1)
⊢ t.IsLE ((t.eTruncLT.obj ⊥).obj X) n

Tactic:
exact t.isLE_of_isZero (by simp) _

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : ℤ
h : WithBotTop.coe i ≤ WithBotTop.coe (n + 1)
⊢ i ≤ n + 1

Tactic:
simp only [WithBotTop.coe_le_coe] at h

Premises used: WithBotTop.coe_le_coe
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
i : ℤ
h : i ≤ n + 1
coe : t.IsLE ((t.truncLT i).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n

Tactic:
dsimp