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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊥
hab : True
⊢ 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))

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_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 : ℤ
hab_1 : ⊥ ⟶ WithBotTop.coe a
hab : True
⊢ t.truncGEπ a ≫ t.truncGEδLT a =
    CategoryStruct.comp (Y := 0 ⋙ shiftFunctor C (A := ℤ) 1) 0 (Functor.whiskerRight 0 (shiftFunctor C (A := ℤ) 1))

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊤
hab : True
⊢ 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)))

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_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 : ℤ
hab_1 : WithBotTop.coe a ⟶ ⊥
hab : WithBotTop.coe a ≤ ⊥
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (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 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)

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 a_1 : ℤ
hab_1 : WithBotTop.coe a ⟶ WithBotTop.coe a_1
hab : WithBotTop.coe a ≤ WithBotTop.coe a_1
⊢ a ≤ a_1

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
a a_1 : ℤ
hab_1 : WithBotTop.coe a ⟶ WithBotTop.coe a_1
hab : a ≤ a_1
coe :
  t.natTransTruncGEOfLE a a_1 ⋯ ≫ t.truncGEδLT a_1 =
    t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a a_1 ⋯) (shiftFunctor C (A := ℤ) 1)
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a_1))
    (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_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) ≫
      (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
coe :
  CategoryStruct.comp (Y := 0) 0 0 = t.truncGEδLT a ≫ Functor.whiskerRight (t.truncLTι a) (shiftFunctor C (A := ℤ) 1)
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (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 (WithBotTop.coe a) ≫
      (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 a_1 : ℤ
hab_1 : WithBotTop.coe a ⟶ WithBotTop.coe a_1
hab : a ≤ a_1
⊢ t.natTransTruncGEOfLE a a_1 ⋯ ≫ t.truncGEδLT a_1 =
    t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a a_1 ⋯) (shiftFunctor C (A := ℤ) 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_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 : ℤ
hab_1 : WithBotTop.coe a ⟶ ⊤
hab : True
⊢ CategoryStruct.comp (Y := 0) 0 0 = t.truncGEδLT a ≫ Functor.whiskerRight (t.truncLTι a) (shiftFunctor C (A := ℤ) 1)

Tactic:
simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_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
n : ℤ
⊢ t.eTruncGEδLT.app (WithBotTop.coe n) = t.truncGEδLT 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
⊢ Eq (α := t.eTruncLT.obj ⊥ ⟶ 𝟭 C) (t.eTruncLTι ⊥) 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ι (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
⊢ t.eTruncLTι ⊤ = 𝟙 (t.eTruncLT.obj ⊤)

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
i : EInt
X Y : C
f : X ⟶ Y
⊢ (t.eTruncLT.obj i).map f ≫ (t.eTruncLTι i).app Y = (t.eTruncLTι i).app X ≫ f

Tactic:
(t.eTruncLTι i).naturality f

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLTι, CategoryTheory.NatTrans.naturality
-- 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
⊢ IsIso (C := Functor.{v_1, v_1, u_1, u_1} C C) (X := 𝟭 C) (𝟙 (𝟭 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
i j : EInt
f : i ⟶ j
X : C
simp : (t.eTruncLT.map (f ≫ homOfLE ⋯)).app X = (t.eTruncLTι i).app X
⊢ (t.eTruncLT.map f).app X ≫ (t.eTruncLTι j).app X = (t.eTruncLTι i).app X

Tactic:
simp only [← NatTrans.comp_app, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_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
⊢ (t.eTruncLT.map (f ≫ homOfLE ⋯)).app X = (t.eTruncLTι i).app X

Tactic:
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
X : C
⊢ (t.eTruncLT.obj ⊥).map (NatTrans.app (t.eTruncLTι ⊥) X) = NatTrans.app (t.eTruncLTι ⊥) ((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
X : C
a : ℤ
⊢ (t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) X) =
    NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) ((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
X : C
⊢ Eq (α :=
    (t.eTruncLT.obj ⊤).obj ((t.eTruncLT.obj ⊤).obj X) ⟶
      (t.eTruncLT.obj ⊤).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
    ((t.eTruncLT.obj ⊤).map (NatTrans.app (t.eTruncLTι ⊤) X)) (NatTrans.app (t.eTruncLTι ⊤) ((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
bot : (t.eTruncLT.obj ⊥).map (NatTrans.app (t.eTruncLTι ⊥) X) = NatTrans.app (t.eTruncLTι ⊥) ((t.eTruncLT.obj ⊥).obj X)
coe :
  ∀ (a : ℤ),
    (t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) X) =
      NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X)
top :
  Eq (α :=
    (t.eTruncLT.obj ⊤).obj ((t.eTruncLT.obj ⊤).obj X) ⟶
      (t.eTruncLT.obj ⊤).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
    ((t.eTruncLT.obj ⊤).map (NatTrans.app (t.eTruncLTι ⊤) X)) (NatTrans.app (t.eTruncLTι ⊤) ((t.eTruncLT.obj ⊤).obj X))
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)

Tactic:
induction i 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
⊢ Eq (α := 𝟭 C ⟶ t.eTruncGE.obj ⊥) (t.eTruncGEπ ⊥) (𝟙 (𝟭 C))

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π (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
⊢ Eq (α := 𝟭 C ⟶ t.eTruncGE.obj ⊤) (t.eTruncGEπ ⊤) 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
i : EInt
X Y : C
f : X ⟶ Y
⊢ (t.eTruncGEπ i).app X ≫ (t.eTruncGE.obj i).map f = f ≫ (t.eTruncGEπ i).app Y

Tactic:
((t.eTruncGEπ i).naturality f).symm

Premises used: CategoryTheory.Triangulated.TStructure.eTruncGEπ, CategoryTheory.NatTrans.naturality, Eq.symm
-- 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
simp : (t.eTruncGE.map (homOfLE ⋯ ≫ f)).app X = (t.eTruncGEπ j).app X
⊢ (t.eTruncGEπ i).app X ≫ (t.eTruncGE.map f).app X = (t.eTruncGEπ j).app X

Tactic:
simp only [← NatTrans.comp_app, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_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
⊢ (t.eTruncGE.map (homOfLE ⋯ ≫ f)).app X = (t.eTruncGEπ j).app X

Tactic:
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
X : C
⊢ Eq (α :=
    (t.eTruncGE.obj ⊥).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) X)) (NatTrans.app (t.eTruncGEπ ⊥) ((t.eTruncGE.obj ⊥).obj X))

Tactic:
simp [truncGE_map_truncGEπ_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_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
a : ℤ
⊢ (t.eTruncGE.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) X) =
    NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) ((t.eTruncGE.obj (WithBotTop.coe a)).obj X)

Tactic:
simp [truncGE_map_truncGEπ_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_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
⊢ (t.eTruncGE.obj ⊤).map (NatTrans.app (t.eTruncGEπ ⊤) X) = NatTrans.app (t.eTruncGEπ ⊤) ((t.eTruncGE.obj ⊤).obj X)

Tactic:
simp [truncGE_map_truncGEπ_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_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
bot :
  Eq (α :=
    (t.eTruncGE.obj ⊥).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) X)) (NatTrans.app (t.eTruncGEπ ⊥) ((t.eTruncGE.obj ⊥).obj X))
coe :
  ∀ (a : ℤ),
    (t.eTruncGE.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) X) =
      NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) ((t.eTruncGE.obj (WithBotTop.coe a)).obj X)
top : (t.eTruncGE.obj ⊤).map (NatTrans.app (t.eTruncGEπ ⊤) X) = NatTrans.app (t.eTruncGEπ ⊤) ((t.eTruncGE.obj ⊤).obj X)
⊢ (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)

Tactic:
induction i using WithBotTop.rec with simp [truncGE_map_truncGEπ_app]

Premises used: CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_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
dsimp :
  (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)
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι j).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)

Tactic:
dsimp [eTruncLTι]

Premises used: 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
i j : EInt
f : i ⟶ j
X : C
⊢ homOfLE ⋯ = f ≫ homOfLE ⋯

Tactic:
rfl