awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ t.natTransTriangleLTGEOfLE a b hab ≫ t.natTransTriangleLTGEOfLE b c hbc = t.natTransTriangleLTGEOfLE a c ⋯

Tactic:
TruncAux.triangleFunctorNatTransOfLE_trans t a b c hab hbc

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_trans, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap, CategoryTheory.Pretriangulated.Triangle.functorHomMk', CategoryTheory.Pretriangulated.Triangle.functorHomMk, CategoryTheory.Triangulated.TStructure.triangleLTGE, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE, CategoryTheory.Pretriangulated.Triangle.functorMk, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE, Classical.choose, CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
⊢ t.natTransTruncLTOfLE a a ⋯ = 𝟙 (t.truncLT a)

Tactic:
congr_arg (fun x ↦ Functor.whiskerRight x (Triangle.π₁)) (t.natTransTriangleLTGEOfLE_refl a)

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap, CategoryTheory.Pretriangulated.Triangle.functorHomMk', CategoryTheory.Pretriangulated.Triangle.π₁, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, CategoryTheory.Triangulated.TStructure.truncLT, congr_arg, CategoryTheory.Functor.whiskerRight, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE, CategoryTheory.Pretriangulated.Triangle.functorMk, CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE, Classical.choose, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_refl, CategoryTheory.NatTrans.id, CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ t.natTransTruncLTOfLE a b hab ≫ t.natTransTruncLTOfLE b c hbc = t.natTransTruncLTOfLE a c ⋯

Tactic:
congr_arg (fun x ↦ Functor.whiskerRight x Triangle.π₁)
    (t.natTransTriangleLTGEOfLE_trans a b c hab hbc)

Premises used: CategoryTheory.NatTrans.vcomp, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap, CategoryTheory.Pretriangulated.Triangle.functorHomMk', CategoryTheory.Pretriangulated.Triangle.π₁, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, CategoryTheory.Triangulated.TStructure.truncLT, congr_arg, CategoryTheory.Functor.whiskerRight, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE, CategoryTheory.Pretriangulated.Triangle.functorMk, CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE, Classical.choose, CategoryTheory.Pretriangulated.Triangle.mk, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_trans
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
⊢ t.natTransTruncGEOfLE a a ⋯ = 𝟙 (t.truncGE a)

Tactic:
congr_arg (fun x ↦ Functor.whiskerRight x (Triangle.π₃)) (t.natTransTriangleLTGEOfLE_refl a)

Premises used: CategoryTheory.Pretriangulated.Triangle.π₃, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap, CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Pretriangulated.Triangle.functorHomMk', _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, congr_arg, CategoryTheory.Functor.whiskerRight, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE, CategoryTheory.Pretriangulated.Triangle.functorMk, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE, CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE, Classical.choose, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_refl, CategoryTheory.NatTrans.id, CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ t.natTransTruncGEOfLE a b hab ≫ t.natTransTruncGEOfLE b c hbc = t.natTransTruncGEOfLE a c ⋯

Tactic:
congr_arg (fun x ↦ Functor.whiskerRight x Triangle.π₃)
    (t.natTransTriangleLTGEOfLE_trans a b c hab hbc)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Pretriangulated.Triangle.π₃, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap, CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Pretriangulated.Triangle.functorHomMk', _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE, congr_arg, CategoryTheory.Functor.whiskerRight, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE, CategoryTheory.Pretriangulated.Triangle.functorMk, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE, CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE, Classical.choose, CategoryTheory.Pretriangulated.Triangle.mk, CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_trans
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
X : C
⊢ a ≤ a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
X : C
⊢ (t.natTransTruncLTOfLE a a ⋯).app X = 𝟙 ((t.truncLT a).obj X)

Tactic:
congr_app (t.natTransTruncLTOfLE_refl a) X

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.natTransTruncLTOfLE a b hab).app X ≫ (t.natTransTruncLTOfLE b c hbc).app X = (t.natTransTruncLTOfLE a c ⋯).app X

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

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
X : C
⊢ (t.natTransTruncGEOfLE a a ⋯).app X = 𝟙 ((t.truncGE a).obj X)

Tactic:
congr_app (t.natTransTruncGEOfLE_refl a) X

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.natTransTruncGEOfLE a b hab).app X ≫ (t.natTransTruncGEOfLE b c hbc).app X = (t.natTransTruncGEOfLE a c ⋯).app X

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

Premises used: CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
hX : IsZero.{v, u} X
n : ℤ
⊢ t.IsLE X n

Tactic:
t.isLE_of_iso (((t.truncLT (n + 1)).map_isZero hX).isoZero ≪≫ hX.isoZero.symm) n

Premises used: CategoryTheory.Functor.map_isZero, CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Triangulated.TStructure.isLE_of_iso, HAdd.hAdd, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, OfNat.ofNat, CategoryTheory.Limits.IsZero.isoZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
X : C
hX : IsZero.{v, u} X
n : ℤ
⊢ t.IsGE X n

Tactic:
t.isGE_of_iso (((t.truncGE n).map_isZero hX).isoZero ≪≫ hX.isoZero.symm) n

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.Functor.map_isZero, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsZero.isoZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
⊢ t.IsLE 0 n

Tactic:
t.isLE_of_isZero (isZero_zero C) n

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Triangulated.TStructure.isLE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
⊢ t.IsGE 0 n

Tactic:
t.isGE_of_isZero (isZero_zero C) n

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Triangulated.TStructure.isGE_of_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
subst : t.IsLE X n₀ ↔ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
⊢ t.IsLE X n₀ ↔ IsIso ((t.truncLTι n₁).app X)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
⊢ t.IsLE X n₀ ↔ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)

Tactic:
⟨fun _ ↦ ?_,
    fun _ ↦ t.isLE_of_iso (asIso (((t.truncLTι (n₀ + 1))).app X)) n₀⟩

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.isLE_of_iso, HAdd.hAdd, Iff.intro, OfNat.ofNat, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
refine : t.IsLE X n₀ → IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
⊢ t.IsLE X n₀ ↔ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)

Tactic:
refine ⟨fun _ ↦ ?_,
    fun _ ↦ t.isLE_of_iso (asIso (((t.truncLTι (n₀ + 1))).app X)) n₀⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h dsimp : t.IsLE X n₀
⊢ t.IsLE (Triangle.obj₁.{v, u} (contractibleTriangle X)) n₀

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ t.IsLE X n₀

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ t.IsGE 0 (n₀ + 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
dsimp : t.IsLE ((t.truncLT (n₀ + 1)).obj X) n₀
⊢ t.IsLE ((t.triangleLTGE (n₀ + 1)).obj X).obj₁ n₀

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ t.IsLE ((t.truncLT (n₀ + 1)).obj X) n₀

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
dsimp : t.IsGE ((t.truncGE (n₀ + 1)).obj X) (n₀ + 1)
⊢ t.IsGE ((t.triangleLTGE (n₀ + 1)).obj X).obj₃ (n₀ + 1)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ t.IsGE ((t.truncGE (n₀ + 1)).obj X) (n₀ + 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
obtain :
  ∀ (e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X) (he : e.hom.hom₂ = Iso.hom (Iso.refl X)),
    IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
⊢ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)

Tactic:
obtain ⟨e, he⟩ := t.triangle_iso_exists
    (contractible_distinguished X) (t.triangleLTGE_distinguished (n₀ + 1) X)
    (Iso.refl X) n₀ (n₀ + 1)
    (by dsimp; infer_instance) (by dsimp; infer_instance)
    (by dsimp; infer_instance) (by dsimp; infer_instance)

Premises used: CategoryTheory.Triangulated.TStructure.triangle_iso_exists, CategoryTheory.Iso.refl, HAdd.hAdd, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Pretriangulated.contractible_distinguished, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
rw : TriangleMorphism.hom₂ (𝟙 ((t.triangleLTGE (n₀ + 1)).obj X)) = 𝟙 X ≫ Iso.hom (Iso.refl X)
⊢ e.inv.hom₂ = 𝟙 X

Tactic:
rw [← cancel_mono e.hom.hom₂, ← comp_hom₂, e.inv_hom_id, he]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Pretriangulated.comp_hom₂, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
⊢ TriangleMorphism.hom₂ (𝟙 ((t.triangleLTGE (n₀ + 1)).obj X)) = 𝟙 X ≫ Iso.hom (Iso.refl X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
⊢ e.inv.hom₂ = 𝟙 X

Tactic:
have he' : e.inv.hom₂ = 𝟙 X := by
    rw [← cancel_mono e.hom.hom₂, ← comp_hom₂, e.inv_hom_id, he]
    simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
he' : e.inv.hom₂ = 𝟙 X
⊢ NatTrans.app (t.truncLTι (n₀ + 1)) X = e.inv.hom₁

Tactic:
simpa [he'] using e.inv.comm₁

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
he' : e.inv.hom₂ = 𝟙 X
⊢ NatTrans.app (t.truncLTι (n₀ + 1)) X = e.inv.hom₁

Tactic:
have : (t.truncLTι (n₀ + 1)).app X = e.inv.hom₁ := by
    simpa [he'] using e.inv.comm₁
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
he' : e.inv.hom₂ = 𝟙 X
this : NatTrans.app (t.truncLTι (n₀ + 1)) X = e.inv.hom₁
rw : IsIso e.inv.hom₁
⊢ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
he' : e.inv.hom₂ = 𝟙 X
this : NatTrans.app (t.truncLTι (n₀ + 1)) X = e.inv.hom₁
⊢ IsIso e.inv.hom₁

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
mp : t.IsGE X n → IsIso ((t.truncGEπ n).app X)
mpr : IsIso ((t.truncGEπ n).app X) → t.IsGE X n
⊢ t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h dsimp : t.IsGE X n
⊢ t.IsGE (Triangle.obj₃.{v, u} (Triangle.invRotate (contractibleTriangle X))) n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
h : t.IsGE X n
⊢ t.IsGE X n

Tactic:
infer_instance