awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
            SpectralObject._proof_2 SpectralObject._proof_4)
          (mk₂ f g)))
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
            SpectralObject._proof_4 SpectralObject._proof_4)
          (mk₂ f g)))
      (NatTrans.app
        { app := fun (D : ComposableArrows EInt 2) ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }
        (mk₂ f g)))

Tactic:
t.triangleω₁δ_distinguished a b c (leOfHom f) (leOfHom g) X

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, Set.Mem, CategoryTheory.Triangulated.TStructure.triangleω₁δ_distinguished, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.homOfLE, CategoryTheory.ComposableArrows.Mk₁.map, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.leOfHom, CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
            SpectralObject._proof_2 SpectralObject._proof_4)
          (mk₂ f g)))
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
            SpectralObject._proof_4 SpectralObject._proof_4)
          (mk₂ f g)))
      (NatTrans.app
        { app := fun (D : ComposableArrows EInt 2) ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }
        (mk₂ f g)))

Tactic:
exact t.triangleω₁δ_distinguished a b c (leOfHom f) (leOfHom g) X

Premises used: CategoryTheory.Triangulated.TStructure.triangleω₁δ_distinguished, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
⊢ (t.spectralObject X).δ f g = NatTrans.app (t.ω₁δ a b c ⋯ ⋯) X

Tactic:
rfl

Premises used: CategoryTheory.Triangulated.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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.truncLT (n + 1)).Additive

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 b : ℤ
hn : a ≤ b
⊢ t.IsLE ((t.truncLE a).obj X) b

Tactic:
t.isLE_truncLT_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isLE_truncLT_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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
⊢ t.IsLE ((t.truncLE n).obj X) n

Tactic:
t.isLE_truncLE_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isLE_truncLE_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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.truncGE (n + 1)).Additive

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 b : ℤ
hn : b ≤ a + 1
⊢ t.IsGE ((t.truncGT a).obj X) b

Tactic:
t.isGE_truncGE_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isGE_truncGE_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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
⊢ t.IsGE ((t.truncGT n).obj X) (n + 1)

Tactic:
t.isGE_truncGT_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isGE_truncGT_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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
⊢ t.IsGE ((t.truncGT (n - 1)).obj X) n

Tactic:
t.isGE_truncGT_obj ..

Premises used: CategoryTheory.Triangulated.TStructure.isGE_truncGT_obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
rw : t.truncLE a = t.truncLT (a + 1)
⊢ t.truncLE a = t.truncLT b

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
⊢ t.truncLE a = t.truncLT (a + 1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
rw : t.truncGT a = t.truncGE (a + 1)
⊢ t.truncGT a = t.truncGE b

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
⊢ t.truncGT a = t.truncGE (a + 1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
subst : (t.truncLEIsoTruncLT a (a + 1) ⋯).hom ≫ t.truncLTι (a + 1) = t.truncLEι a
⊢ (t.truncLEIsoTruncLT a b h).hom ≫ t.truncLTι b = t.truncLEι a

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
rw rw₁ : Eq (α := t.truncLE a ⟶ 𝟭 C) (t.truncLTι (a + 1)) (t.truncLTι (a + 1))
⊢ 𝟙 (t.truncLE a) ≫ t.truncLTι (a + 1) = t.truncLTι (a + 1)

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
X : C
⊢ (t.truncLEIsoTruncLT a b h).hom.app X ≫ (t.truncLTι b).app X = (t.truncLEι a).app X

Tactic:
congr_app (t.truncLEIsoTruncLT_hom_ι a b h) X

Premises used: CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
subst : (t.truncLEIsoTruncLT a (a + 1) ⋯).inv ≫ t.truncLEι a = t.truncLTι (a + 1)
⊢ (t.truncLEIsoTruncLT a b h).inv ≫ t.truncLEι a = t.truncLTι b

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
rw rw₁ : Eq (α := t.truncLT (a + 1) ⟶ 𝟭 C) (t.truncLTι (a + 1)) (t.truncLTι (a + 1))
⊢ 𝟙 (t.truncLT (a + 1)) ≫ t.truncLTι (a + 1) = t.truncLTι (a + 1)

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
X : C
⊢ (t.truncLEIsoTruncLT a b h).inv.app X ≫ (t.truncLEι a).app X = (t.truncLTι b).app X

Tactic:
congr_app (t.truncLEIsoTruncLT_inv_ι a b h) X

Premises used: CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a ≤ b
⊢ a + 1 ≤ b + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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₀ n₁ : ℤ
h : n₀ ≤ n₁
X : C
⊢ (t.natTransTruncLEOfLE n₀ n₁ h).app X ≫ (t.truncLEι n₁).app X = (t.truncLEι n₀).app X

Tactic:
t.natTransTruncLTOfLE_ι_app _ _ _ _

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 ≤ a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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.natTransTruncLEOfLE a a ⋯ = 𝟙 (t.truncLE a)

Tactic:
t.natTransTruncLTOfLE_refl _

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl, CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE, CategoryTheory.Triangulated.TStructure.truncLE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ t.natTransTruncLEOfLE a b hab ≫ t.natTransTruncLEOfLE b c hbc = t.natTransTruncLEOfLE a c ⋯

Tactic:
t.natTransTruncLTOfLE_trans _ _ _ _ _

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans, CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE, CategoryTheory.Triangulated.TStructure.truncLE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
X : C
⊢ a ≤ a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
X : C
⊢ (t.natTransTruncLEOfLE a a ⋯).app X = 𝟙 ((t.truncLE a).obj X)

Tactic:
congr_app (t.natTransTruncLEOfLE_refl a) X

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 c : ℤ
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.natTransTruncLEOfLE a b hab).app X ≫ (t.natTransTruncLEOfLE b c hbc).app X = (t.natTransTruncLEOfLE a c ⋯).app X

Tactic:
congr_app (t.natTransTruncLEOfLE_trans a b c hab hbc) X

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
subst : t.truncGTπ a ≫ (t.truncGTIsoTruncGE a (a + 1) ⋯).hom = t.truncGEπ (a + 1)
⊢ t.truncGTπ a ≫ (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
rw rw₁ : Eq (α := 𝟭 C ⟶ t.truncGE (a + 1)) (t.truncGEπ (a + 1)) (t.truncGEπ (a + 1))
⊢ t.truncGEπ (a + 1) ≫ 𝟙 (t.truncGT a) = t.truncGEπ (a + 1)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
X : C
⊢ (t.truncGTπ a).app X ≫ (t.truncGTIsoTruncGE a b h).hom.app X = (t.truncGEπ b).app X

Tactic:
congr_app (t.π_truncGTIsoTruncGE_hom a b h) X

Premises used: CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
subst : t.truncGEπ (a + 1) ≫ (t.truncGTIsoTruncGE a (a + 1) ⋯).inv = t.truncGTπ a
⊢ t.truncGEπ b ≫ (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
rw rw₁ : Eq (α := 𝟭 C ⟶ t.truncGE (a + 1)) (t.truncGEπ (a + 1)) (t.truncGEπ (a + 1))
⊢ t.truncGEπ (a + 1) ≫ 𝟙 (t.truncGE (a + 1)) = t.truncGEπ (a + 1)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
X : C
⊢ (t.truncGEπ b).app X ≫ (t.truncGTIsoTruncGE a b h).inv.app X = (t.truncGTπ a).app X

Tactic:
congr_app (t.π_truncGTIsoTruncGE_inv a b h) X

Premises used: CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
refine_1 :
  (t.triangleLEGE a b h).whiskerLeft Triangle.π₁Toπ₂ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) =
    (t.truncLEIsoTruncLT a b h).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₁Toπ₂
refine_2 :
  (t.triangleLEGE a b h).whiskerLeft Triangle.π₂Toπ₃ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) =
    Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₂Toπ₃
refine_3 :
  (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1) =
    Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁
⊢ t.triangleLEGE a b h ≅ t.triangleLTGE b

Tactic:
refine Triangle.functorIsoMk _ _ (t.truncLEIsoTruncLT a b h) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
refine_3 :
  ∀ (x : C),
    ((t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
            Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1)).app
        x =
      (Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁).app x
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1) =
    Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
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 : ℤ
h : a + 1 = b
x : C
refine_3 :
  ((t.truncGEδLT b).app x ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLEIsoTruncLT a b h).inv.app x)) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLEIsoTruncLT a b h).hom.app x) =
    𝟙 ((t.truncGE b).obj x) ≫ (t.truncGEδLT b).app x
⊢ ((t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1)).app
      x =
    (Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁).app x

Tactic:
dsimp [truncGEδLE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGEδLE