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
y : EInt
f : ⊥ ⟶ y
bot :
  (f : Quiver.Hom (V := EInt) ⊥ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
bot₁ :
  (b : ℤ) →
    (f : ⊥ ⟶ WithBotTop.coe b) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
            (WithBotTop.coe b) :
          Functor.{v_1, v_1, u_1, u_1} C C)
bot₂ :
  (f : Quiver.Hom (V := EInt) ⊥ ⊤) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | top => exact 0

Premises used: CategoryTheory.CategoryStruct.id
-- 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
a : ℤ
f : WithBotTop.coe a ⟶ ⊥
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact 0
-- 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
a b : ℤ
f : WithBotTop.coe a ⟶ WithBotTop.coe b
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
        (WithBotTop.coe b) :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE
-- 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
a : ℤ
f : WithBotTop.coe a ⟶ ⊤
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact 0
-- 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
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
coe :
  (f : WithBotTop.coe a ⟶ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
          (WithBotTop.coe a) :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
coe₁ :
  (b : ℤ) →
    (f : WithBotTop.coe a ⟶ WithBotTop.coe b) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
            (WithBotTop.coe a) :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
            (WithBotTop.coe b) :
          Functor.{v_1, v_1, u_1, u_1} C C)
coe₂ :
  (f : WithBotTop.coe a ⟶ ⊤) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
          (WithBotTop.coe a) :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | top => exact 0
-- 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
f : Quiver.Hom (V := EInt) ⊤ ⊥
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact 0
-- 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
b : ℤ
f : ⊤ ⟶ WithBotTop.coe b
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
        (WithBotTop.coe b) :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact 0
-- 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
f : Quiver.Hom (V := EInt) ⊤ ⊤
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- 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
y : EInt
f : ⊤ ⟶ y
top :
  (f : Quiver.Hom (V := EInt) ⊤ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
top₁ :
  (b : ℤ) →
    (f : ⊤ ⟶ WithBotTop.coe b) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
            (WithBotTop.coe b) :
          Functor.{v_1, v_1, u_1, u_1} C C)
top₂ :
  (f : Quiver.Hom (V := EInt) ⊤ ⊤) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- 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 y : EInt
f : x ⟶ y
bot :
  (f : ⊥ ⟶ y) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
        Functor.{v_1, v_1, u_1, u_1} C C)
coe :
  (a : ℤ) →
    (f : WithBotTop.coe a ⟶ y) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
            (WithBotTop.coe a) :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
          Functor.{v_1, v_1, u_1, u_1} C C)
top :
  (f : ⊤ ⟶ y) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 x :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | top => exact 0
    | coe a =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | top => exact 0
    | top =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- 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
⊢ t.eTruncGE.obj ⊥ = 𝟭 C

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, WithBotTop.rec, 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
⊢ t.eTruncGE.obj ⊤ = 0

Tactic:
rfl

Premises used: WithBotTop.rec, 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
n : ℤ
⊢ t.eTruncGE.obj (WithBotTop.coe n) = t.truncGE n

Tactic:
rfl

Premises used: WithBotTop.rec, 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
bot : (t.eTruncGE.obj ⊥).Additive
coe : ∀ (a : ℤ), (t.eTruncGE.obj (WithBotTop.coe a)).Additive
top : (t.eTruncGE.obj ⊤).Additive
⊢ (t.eTruncGE.obj i).Additive

Tactic:
induction i using WithBotTop.rec
-- 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
a : ℤ
⊢ (t.truncGE a).Additive

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
a b : EInt
hab : a ⟶ b
⊢ a ≤ b

Tactic:
replace hab := leOfHom hab
-- 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
b : EInt
hab_1 : ⊤ ⟶ b
hab : ⊤ ≤ b
⊢ Eq (α :=
    t.eTruncGE.obj ⊤ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊤ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)

Tactic:
apply (isZero_zero _).eq_of_src

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.eq_of_src
-- 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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊥
hab : LE.le (α := EInt) ⊥ ⊥
⊢ True

Tactic:
simp at hab
-- 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
a : ℤ
hab_1 : ⊥ ⟶ WithBotTop.coe a
hab : ⊥ ≤ WithBotTop.coe a
⊢ True

Tactic:
simp at hab
-- 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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊤
hab : LE.le (α := EInt) ⊥ ⊤
⊢ True

Tactic:
simp at hab
-- 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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊥
hab : True
bot :
  Eq (α := Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) (0 ⋙ shiftFunctor C (A := ℤ) 1)) (𝟙 (𝟭 C) ≫ 0)
    (0 ≫ Functor.whiskerRight (𝟙 0) (shiftFunctor C (A := ℤ) 1))
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)

Tactic:
dsimp [eTruncGE, eTruncLT]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Triangulated.TStructure.eTruncLT
-- 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
a : ℤ
hab_1 : ⊥ ⟶ WithBotTop.coe a
hab : True
bot :
  t.truncGEπ a ≫ t.truncGEδLT a =
    CategoryStruct.comp (Y := 0 ⋙ shiftFunctor C (A := ℤ) 1) 0 (Functor.whiskerRight 0 (shiftFunctor C (A := ℤ) 1))
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a))
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)

Tactic:
dsimp [eTruncGE, eTruncLT]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Triangulated.TStructure.eTruncLT
-- 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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊤
hab : True
bot :
  Eq (α := Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) (𝟭 C ⋙ shiftFunctor C (A := ℤ) 1))
    (CategoryStruct.comp (Y := 0) 0 0)
    (CategoryStruct.comp (Y := 0 ⋙ shiftFunctor C (A := ℤ) 1) 0 (Functor.whiskerRight 0 (shiftFunctor C (A := ℤ) 1)))
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊤)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊤)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)

Tactic:
dsimp [eTruncGE, eTruncLT]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Triangulated.TStructure.eTruncLT