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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
x x_1 : C
x_2 : x ⟶ x_1
⊢ ((t.truncGE a).map ((t.truncLT b).map x_2) ≫
        t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x_1 ≫ (t.truncGEπ a).app x_1) a) (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1) =
    (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x ≫ (t.truncGEπ a).app x) a) (b - 1) b ⋯ ≫
        (t.truncLT b).map ((t.truncGE a).map x_2)) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1)

Tactic:
exact t.from_truncGE_obj_ext (by simp)

Premises used: CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app X

Tactic:
simp [truncGELTToLTGE]

Premises used: CategoryTheory.Triangulated.TStructure.truncGELTToLTGE
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X
hφ :
  (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app X
dsimp :
  (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)
⊢ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X
hφ :
  (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app X
⊢ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
exact t.from_truncGE_obj_ext (by cat_disch)

Premises used: CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
rw :
  (t.truncGELTToLTGE a b).app X =
    inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ≫
      (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))
⊢ (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X =
    (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))

Tactic:
rw [← cancel_epi (inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))),
    IsIso.inv_hom_id_assoc]

Premises used: CategoryTheory.Triangulated.TStructure.truncGE, CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.inv, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ (t.truncGEπ a).app ((t.truncLT b).obj X) ≫
      (inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ≫
          (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))) ≫
        (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ (t.truncGELTToLTGE a b).app X =
    inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ≫
      (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))

Tactic:
exact t.truncGELTToLTGE_app_pentagon_uniqueness _ (by simp)

Premises used: CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_uniqueness
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
⊢ IsIso ((t.truncLT a).map ((t.truncLTι b).app X))

Tactic:
have := t.isIso_truncLT_map_truncLTι_app a b h X
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLTLTGELT a b h).obj X)

Tactic:
isomorphic_distinguished _ (t.triangleLTGE_distinguished a ((t.truncLT b).obj X)) _ ?_

Premises used: CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Functor.obj
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
refine : (t.triangleLTLTGELT a b h).obj X ≅ (t.triangleLTGE a).obj ((t.truncLT b).obj X)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLTLTGELT a b h).obj X)

Tactic:
refine isomorphic_distinguished _ (t.triangleLTGE_distinguished a ((t.truncLT b).obj X)) _ ?_

Premises used: CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.triangleLTGE_distinguished, CategoryTheory.Functor.obj
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ ((t.triangleLTLTGELT a b h).obj X).mor₂ ≫ Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₃) =
    Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₂) ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₂

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ ((t.triangleLTLTGELT a b h).obj X).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm.hom =
    Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₃) ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₃

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
refine :
  ((t.triangleLTLTGELT a b h).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₂) =
    (asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm.hom ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₁
⊢ (t.triangleLTLTGELT a b h).obj X ≅ (t.triangleLTGE a).obj ((t.truncLT b).obj X)

Tactic:
refine Triangle.isoMk _ _ ((asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm)
    (Iso.refl _) (Iso.refl _) ?_ (by simp) (by simp)

Premises used: CategoryTheory.Triangulated.TStructure.truncLTι, CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Iso.symm, 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
dsimp :
  (t.natTransTruncLTOfLE a b h).app X ≫ 𝟙 ((t.truncLT b).obj X) =
    inv ((t.truncLT a).map ((t.truncLTι b).app X)) ≫ (t.truncLTι a).app ((t.truncLT b).obj X)
⊢ ((t.triangleLTLTGELT a b h).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₂) =
    (asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm.hom ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₁

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
simp :
  (t.truncLT a).map ((t.truncLTι b).app X) ≫ (t.natTransTruncLTOfLE a b h).app X =
    (t.truncLTι a).app ((t.truncLT b).obj X)
⊢ (t.natTransTruncLTOfLE a b h).app X ≫ 𝟙 ((t.truncLT b).obj X) =
    inv ((t.truncLT a).map ((t.truncLTι b).app X)) ≫ (t.truncLTι a).app ((t.truncLT b).obj X)

Tactic:
simp only [Category.comp_id, IsIso.eq_inv_comp]

Premises used: CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Category.comp_id
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ ((t.truncLT a).map ((t.truncLTι b).app X) ≫ (t.natTransTruncLTOfLE a b h).app X) ≫ (t.truncLTι b).app X =
    (t.truncLTι a).app ((t.truncLT b).obj X) ≫ (t.truncLTι b).app 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ (t.truncLT a).map ((t.truncLTι b).app X) ≫ (t.natTransTruncLTOfLE a b h).app X =
    (t.truncLTι a).app ((t.truncLT b).obj X)

Tactic:
exact t.to_truncLT_obj_ext (by simp)

Premises used: CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
rw : ∀ (X : C), IsIso ((t.truncGELTToLTGE a b).app X)
⊢ IsIso (t.truncGELTToLTGE a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
pos : ∀ (h : a ≤ b), IsIso ((t.truncGELTToLTGE a b).app X)
neg : ∀ (h : ¬a ≤ b), IsIso ((t.truncGELTToLTGE a b).app X)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
by_cases h : a ≤ b
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
⊢ u₁₂ ≫ u₂₃ = u₁₃

Tactic:
simp [u₁₂, u₂₃, u₁₃]
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
⊢ u₁₂ ≫ u₂₃ = u₁₃

Tactic:
have eq : u₁₂ ≫ u₂₃ = u₁₃ := by simp [u₁₂, u₂₃, u₁₃]
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
pos : ∀ (H : Octahedron eq ⋯ ⋯ ⋯), IsIso ((t.truncGELTToLTGE a b).app X)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
have H := someOctahedron eq (t.triangleLTLTGELT_distinguished a b h X)
      (t.triangleLTGE_distinguished b X) (t.triangleLTGE_distinguished a X)
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
dsimp : t.IsGE ((t.truncGE b).obj X) b
⊢ t.IsGE
    (Triangle.mk H.m₁ H.m₃
        ((t.truncGEδLT b).app X ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (((t.truncLT b).whiskerLeft (t.truncGEπ a)).app X))).obj₃
    b

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
⊢ t.IsGE ((t.truncGE b).obj X) b

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
⊢ IsIso ((t.truncLT b).map H.m₁)

Tactic:
have : IsIso ((t.truncLT b).map H.m₁) :=
      t.isIso₁_truncLT_map_of_isGE _ H.mem b (by dsimp; 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ b - 1 + 1 = b

Tactic:
lia
-- 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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
dsimp :
  t.liftTruncLT m₁ (b - 1) b ⋯ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X)
⊢ t.liftTruncLT m₁ (b - 1) b ⋯ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ t.liftTruncLT m₁ (b - 1) b ⋯ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
simpa using H.comm₁

Premises used: CategoryTheory.Triangulated.Octahedron.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
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ t.liftTruncLT m₁ (b - 1) b ⋯ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
exact t.from_truncGE_obj_ext (by simpa using H.comm₁)

Premises used: CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext