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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
dsimp :
  Eq (α := (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj X))
        (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncGE.obj a).obj X) :
          (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj X))
        ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (φ.app 0)) X) ≫ (t.eTruncLTGEIsoGELT a' b').hom.app X :
          (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X)) :
      (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    ((t.eTruncLTGEIsoGELT a b).hom.app X ≫
        CategoryStruct.comp (Y := (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X))
          (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj X))
          ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) X)) :
      (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
⊢ Eq (α :=
    (t.eTruncLT.obj ((mk₁ (homOfLE hab)).obj 1)).obj ((t.eTruncGE.obj a).obj X) ⟶
      (t.eTruncLT.obj b' ⋙ t.eTruncGE.obj a').obj X)
    (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncGE.obj a).obj X) ≫
      (t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (φ.app 0)) X) ≫ (t.eTruncLTGEIsoGELT a' b').hom.app X)
    ((t.eTruncLTGEIsoGELT a b).hom.app X ≫
      NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) X))

Tactic:
dsimp
-- 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ Eq (α :=
    (t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b).obj X ⟶
      (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)))
        (NatTrans.app (t.eTruncLT.map (φ.app 1)) ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) :
          (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
            (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)))
        (CategoryStruct.comp (Y := (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X)))
            ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj X)) :
              (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
                (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X)))
            ((t.eTruncLT.obj b').map
                  ((t.eTruncGE.obj a').map
                    (NatTrans.app (t.eTruncLT.map (φ.app 1)) X ≫
                      NatTrans.app (t.eTruncLTι ((mk₁ (homOfLE hab')).obj 1)) X)) ≫
                (t.eTruncLTGEIsoGELT a' b').hom.app X :
              (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X)) ⟶
                (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X)) :
          (t.eTruncLT.obj b').obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
            (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X)) :
      (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
        (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))
    ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
        CategoryStruct.comp (Y := (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X))
          (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj X))
          ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) X)) :
      (t.eTruncLT.obj b).obj ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ⟶
        (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X))

Tactic:
simp [↓Functor.map_comp, t.eTruncLTGEIsoGELT_hom_app_fac]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
⊢ t.heart X ↔ t.IsLE X 0 ∧ t.IsGE X 0

Tactic:
simp [heart]

Premises used: CategoryTheory.Triangulated.TStructure.heart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
h : ∀ (X : C), t.heart.ι.essImage X ↔ t.heart X
⊢ t.heart.ι.essImage = t.heart

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
X : C
⊢ t.heart.ι.essImage X ↔ t.heart X

Tactic:
⟨fun ⟨⟨Y, hY⟩, ⟨e⟩⟩ ↦ t.heart.prop_of_iso e hY,
      fun hX ↦ ⟨⟨X, hX⟩, ⟨Iso.refl _⟩⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Triangulated.TStructure.heart, CategoryTheory.Iso.refl, Nonempty.intro, _private.0.CategoryTheory.Triangulated.TStructure.hasHeartFullSubcategory.match_3, Iff.intro, Exists.intro, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
X : C
⊢ t.heart.ι.essImage X ↔ t.heart X

Tactic:
exact ⟨fun ⟨⟨Y, hY⟩, ⟨e⟩⟩ ↦ t.heart.prop_of_iso e hY,
      fun hX ↦ ⟨⟨X, hX⟩, ⟨Iso.refl _⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
⊢ Functor.Additive.{v', u', v, u} (C := H) t.ιHeart

Tactic:
Heart.additive_ι

Premises used: CategoryTheory.Triangulated.TStructure.Heart.additive_ι, CategoryTheory.Triangulated.TStructure.ιHeart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
⊢ Functor.Full.{v', v, u', u} (C := H) t.ιHeart

Tactic:
Heart.full_ι

Premises used: CategoryTheory.Triangulated.TStructure.Heart.full_ι, CategoryTheory.Triangulated.TStructure.ιHeart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
⊢ Functor.Faithful.{v', v, u', u} (C := H) t.ιHeart

Tactic:
Heart.faithful_ι

Premises used: CategoryTheory.Triangulated.TStructure.ιHeart, CategoryTheory.Triangulated.TStructure.Heart.faithful_ι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
⊢ Functor.essImage.{v', v, u', u} (C := H) t.ιHeart = t.heart

Tactic:
Heart.essImage_eq_heart

Premises used: CategoryTheory.Triangulated.TStructure.ιHeart, CategoryTheory.Triangulated.TStructure.Heart.essImage_eq_heart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
X : H
rw : Functor.essImage.{v', v, u', u} (C := H) t.ιHeart (Functor.obj.{v', v, u', u} t.ιHeart X)
⊢ t.heart (Functor.obj.{v', v, u', u} t.ιHeart X)

Tactic:
rw [← t.essImage_ιHeart H]

Premises used: CategoryTheory.Triangulated.TStructure.essImage_ιHeart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
X : H
⊢ Functor.essImage.{v', v, u', u} (C := H) t.ιHeart (Functor.obj.{v', v, u', u} t.ιHeart X)

Tactic:
t.ιHeart.obj_mem_essImage X

Premises used: CategoryTheory.Functor.obj_mem_essImage, CategoryTheory.Triangulated.TStructure.ιHeart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
X : H
⊢ Functor.essImage.{v', v, u', u} (C := H) t.ιHeart (Functor.obj.{v', v, u', u} t.ιHeart X)

Tactic:
exact t.ιHeart.obj_mem_essImage X

Premises used: CategoryTheory.Functor.obj_mem_essImage, CategoryTheory.Triangulated.TStructure.ιHeart
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
X : H
⊢ t.IsLE (Functor.obj.{v', v, u', u} t.ιHeart X) 0

Tactic:
⟨(t.ιHeart_obj_mem X).1⟩

Premises used: CategoryTheory.Triangulated.TStructure.ιHeart_obj_mem, CategoryTheory.Triangulated.TStructure.IsLE.mk, And.left
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
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
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
X : H
⊢ t.IsGE (Functor.obj.{v', v, u', u} t.ιHeart X) 0

Tactic:
⟨(t.ιHeart_obj_mem X).2⟩

Premises used: CategoryTheory.Triangulated.TStructure.ιHeart_obj_mem, And.right, CategoryTheory.Triangulated.TStructure.IsGE.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
X Y : P.FullSubcategory
f : X ⟶ Y
hX : t.le 0 (X.obj (P := P))
hY : t.ge 1 (Y.obj (P := P))
rw : P.ι.map f = 0
⊢ P.ι.map f = P.ι.map 0

Tactic:
rw [Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
X Y : P.FullSubcategory
f : X ⟶ Y
hX : t.le 0 (X.obj (P := P))
hY : t.ge 1 (Y.obj (P := P))
⊢ P.ι.map f = 0

Tactic:
t.zero' (P.ι.map f) hX hY

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.map, CategoryTheory.Triangulated.TStructure.zero'
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
X Y : P.FullSubcategory
f : X ⟶ Y
hX : t.le 0 (X.obj (P := P))
hY : t.ge 1 (Y.obj (P := P))
⊢ P.ι.map f = 0

Tactic:
exact t.zero' (P.ι.map f) hX hY

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.map, CategoryTheory.Triangulated.TStructure.zero'
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
A : P.FullSubcategory
obtain :
  ∀ (X Y : C) (hX : t.IsLE X 0) (hY : t.IsGE Y 1) (f : X ⟶ A.obj (P := P)) (g : A.obj (P := P) ⟶ Y)
    (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f g h))
    (X' : C) (hX' : P X') (e : X ≅ X') (Y' : C) (hY' : P Y') (e' : Y ≅ Y'),
    ∃ (X : P.FullSubcategory) (Y : P.FullSubcategory) (_ : t.le 0 (X.obj (P := P))) (_ : t.ge 1 (Y.obj (P := P))) (f :
      X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
      Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
        (@distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory P) ⋯ _) (Triangle.mk f g h)
⊢ ∃ (X : P.FullSubcategory) (Y : P.FullSubcategory) (_ : t.le 0 (X.obj (P := P))) (_ : t.ge 1 (Y.obj (P := P))) (f :
    X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
      (@distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory P) ⋯ _) (Triangle.mk f g h)

Tactic:
obtain ⟨X, Y, hX, hY, f, g, h, hT, ⟨X', hX', ⟨e⟩⟩, ⟨Y', hY', ⟨e'⟩⟩⟩ :=
      h.exists_triangle_zero_one A.1 A.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.ObjectProperty.HasInducedTStructure.exists_triangle_zero_one
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h_1 : P.HasInducedTStructure t
A : P.FullSubcategory
X Y : C
hX : t.IsLE X 0
hY : t.IsGE Y 1
f : X ⟶ A.obj (P := P)
g : A.obj (P := P) ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
X' : C
hX' : P X'
e : X ≅ X'
Y' : C
hY' : P Y'
e' : Y ≅ Y'
⊢ ∃ (X : P.FullSubcategory) (Y : P.FullSubcategory) (_ : t.le 0 (X.obj (P := P))) (_ : t.ge 1 (Y.obj (P := P))) (f :
    X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
      (@distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory P) ⋯ _) (Triangle.mk f g h)

Tactic:
⟨⟨X', hX'⟩, ⟨Y', hY'⟩, (t.le 0).prop_of_iso e hX.le,
      (t.ge 1).prop_of_iso e' hY.ge,
      P.fullyFaithfulι.preimage (e.inv ≫ f),
      P.fullyFaithfulι.preimage (g ≫ e'.hom),
      P.fullyFaithfulι.preimage (e'.inv ≫ h ≫ e.hom⟦(1 : ℤ)⟧' ≫
          (P.ι.commShiftIso (1 : ℤ)).inv.app ⟨X', hX'⟩),
      isomorphic_distinguished _ hT _ (Triangle.isoMk _ _ e.symm (Iso.refl _) e'.symm)⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ι, CategoryTheory.shiftFunctor, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.fullyFaithfulι, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, CategoryTheory.Triangulated.TStructure.IsLE.le, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Functor.FullyFaithful.preimage, CategoryTheory.Pretriangulated.isomorphic_distinguished, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Triangulated.TStructure.IsGE.ge, CategoryTheory.Triangulated.TStructure.ge, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Triangulated.TStructure.le
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h_1 : P.HasInducedTStructure t
A : P.FullSubcategory
X Y : C
hX : t.IsLE X 0
hY : t.IsGE Y 1
f : X ⟶ A.obj (P := P)
g : A.obj (P := P) ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
X' : C
hX' : P X'
e : X ≅ X'
Y' : C
hY' : P Y'
e' : Y ≅ Y'
⊢ ∃ (X : P.FullSubcategory) (Y : P.FullSubcategory) (_ : t.le 0 (X.obj (P := P))) (_ : t.ge 1 (Y.obj (P := P))) (f :
    X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
      (@distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory P) ⋯ _) (Triangle.mk f g h)

Tactic:
exact ⟨⟨X', hX'⟩, ⟨Y', hY'⟩, (t.le 0).prop_of_iso e hX.le,
      (t.ge 1).prop_of_iso e' hY.ge,
      P.fullyFaithfulι.preimage (e.inv ≫ f),
      P.fullyFaithfulι.preimage (g ≫ e'.hom),
      P.fullyFaithfulι.preimage (e'.inv ≫ h ≫ e.hom⟦(1 : ℤ)⟧' ≫
          (P.ι.commShiftIso (1 : ℤ)).inv.app ⟨X', hX'⟩),
      isomorphic_distinguished _ hT _ (Triangle.isoMk _ _ e.symm (Iso.refl _) e'.symm)⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
X : P.FullSubcategory
n : ℤ
⊢ TStructure.IsLE (P.tStructure t) X n ↔ t.IsLE (X.obj (P := P)) n

Tactic:
⟨fun h => ⟨h.1⟩, fun h => ⟨h.1⟩⟩

Premises used: CategoryTheory.Triangulated.TStructure.IsLE.mk, CategoryTheory.Triangulated.TStructure.IsLE.le, Iff.intro
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
X : P.FullSubcategory
n : ℤ
⊢ TStructure.IsGE (P.tStructure t) X n ↔ t.IsGE (X.obj (P := P)) n

Tactic:
⟨fun h => ⟨h.1⟩, fun h => ⟨h.1⟩⟩

Premises used: Iff.intro, CategoryTheory.Triangulated.TStructure.IsGE.ge, CategoryTheory.Triangulated.TStructure.IsGE.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced
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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
t : TStructure.{v_1, u_1} C
h : ∀ (X : C), P X → ∀ (n : ℤ), P ((t.truncLE n).obj X) ∧ P ((t.truncGE n).obj X)
X : C
hX : P X
⊢ HAdd.hAdd (α := ℤ) 0 1 = 1

Tactic:
lia