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
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) 0 t.truncLT (𝟭 C) ⊥ :
      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) 0 t.truncLT (𝟭 C)
        (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) 0 t.truncLT (𝟭 C) ⊥ :
      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) 0 t.truncLT (𝟭 C) ⊤ :
      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
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) 0 t.truncLT (𝟭 C) ⊥ :
        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) 0 t.truncLT (𝟭 C) ⊥ :
        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) 0 t.truncLT (𝟭 C) ⊥ :
          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) 0 t.truncLT (𝟭 C)
            (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) 0 t.truncLT (𝟭 C) ⊥ :
        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) 0 t.truncLT (𝟭 C) ⊤ :
        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) 0 t.truncLT (𝟭 C) ⊥ :
      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) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | 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) 0 t.truncLT (𝟭 C)
        (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) 0 t.truncLT (𝟭 C) ⊥ :
      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
⊢ a ≤ b

Tactic:
simpa using leOfHom f

Premises used: CategoryTheory.leOfHom
-- 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) 0 t.truncLT (𝟭 C)
        (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) 0 t.truncLT (𝟭 C)
        (WithBotTop.coe b) :
      Functor.{v_1, v_1, u_1, u_1} C C)

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

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE
-- 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) 0 t.truncLT (𝟭 C)
        (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) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact t.truncLTι a

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι
-- 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) 0 t.truncLT (𝟭 C)
          (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) 0 t.truncLT (𝟭 C) ⊥ :
        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) 0 t.truncLT (𝟭 C)
            (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) 0 t.truncLT (𝟭 C)
            (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) 0 t.truncLT (𝟭 C)
          (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) 0 t.truncLT (𝟭 C) ⊤ :
        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) 0 t.truncLT (𝟭 C)
        (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) 0 t.truncLT (𝟭 C) 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.natTransTruncLTOfLE a b (by simpa using leOfHom f)
      | top => exact t.truncLTι a

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι
-- 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) 0 t.truncLT (𝟭 C) ⊤ :
      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) 0 t.truncLT (𝟭 C) ⊥ :
      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) 0 t.truncLT (𝟭 C) ⊤ :
      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) 0 t.truncLT (𝟭 C)
        (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) 0 t.truncLT (𝟭 C) ⊤ :
      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) 0 t.truncLT (𝟭 C) ⊤ :
      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) 0 t.truncLT (𝟭 C) ⊤ :
        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) 0 t.truncLT (𝟭 C) ⊥ :
        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) 0 t.truncLT (𝟭 C) ⊤ :
          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) 0 t.truncLT (𝟭 C)
            (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) 0 t.truncLT (𝟭 C) ⊤ :
        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) 0 t.truncLT (𝟭 C) ⊤ :
        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) 0 t.truncLT (𝟭 C) ⊤ :
      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) 0 t.truncLT (𝟭 C) 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) 0 t.truncLT (𝟭 C) ⊥ :
        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) 0 t.truncLT (𝟭 C) 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) 0 t.truncLT (𝟭 C)
            (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) 0 t.truncLT (𝟭 C) 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) 0 t.truncLT (𝟭 C) ⊤ :
        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) 0 t.truncLT (𝟭 C) 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) 0 t.truncLT (𝟭 C) 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) 0 t.truncLT (𝟭 C) 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 0
      | top => exact 0
    | coe a =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f)
      | top => exact t.truncLTι a
    | 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
x y z : EInt
f : x ⟶ y
g : y ⟶ z
⊢ x ≤ y

Tactic:
have f' := leOfHom f
-- 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 z : EInt
f : x ⟶ y
g : y ⟶ z
f' : x ≤ y
⊢ y ≤ z

Tactic:
have g' := leOfHom g
-- 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.eTruncLT.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.eTruncLT.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.eTruncLT.obj (WithBotTop.coe n) = t.truncLT 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
n : ℤ
⊢ WithBotTop.coe n ≤ ⊤

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 : ℤ
⊢ t.eTruncLT.map (homOfLE ⋯) = t.truncLTι 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.eTruncLT.obj ⊥).Additive
coe : ∀ (a : ℤ), (t.eTruncLT.obj (WithBotTop.coe a)).Additive
top : (t.eTruncLT.obj ⊤).Additive
⊢ (t.eTruncLT.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
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := C) (D := C) 0

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 : ℤ
⊢ (t.truncLT 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
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (𝟭 C)

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
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
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 t.truncGEπ b

Premises used: CategoryTheory.Triangulated.TStructure.truncGEπ
-- 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