awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
dsimp : t.IsLE (((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₀
⊢ t.IsLE
    (Triangle.obj₁
      (Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
        (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
        (Functor.obj
            (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h :
              P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
            (FullSubcategory.mk (P := P) T.obj₂ h₂) :
          Triangle.{v_1, u_1} P.FullSubcategory)))
    n₀

Tactic:
dsimp
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
rw :
  TStructure.IsLE (P.tStructure t)
    ((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)) n₀
⊢ t.IsLE (((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₀

Tactic:
rw [← P.tStructure_isLE_iff]

Premises used: CategoryTheory.ObjectProperty.tStructure_isLE_iff
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ TStructure.IsLE (P.tStructure t)
    ((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)) n₀

Tactic:
infer_instance
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
dsimp : t.IsGE (((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₁
⊢ t.IsGE
    (Triangle.obj₃
      (Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
        (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
        (Functor.obj
            (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h :
              P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
            (FullSubcategory.mk (P := P) T.obj₂ h₂) :
          Triangle.{v_1, u_1} P.FullSubcategory)))
    n₁

Tactic:
dsimp
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
rw :
  TStructure.IsGE (P.tStructure t)
    ((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)) n₁
⊢ t.IsGE (((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₁

Tactic:
rw [← P.tStructure_isGE_iff]

Premises used: CategoryTheory.ObjectProperty.tStructure_isGE_iff
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ TStructure.IsGE (P.tStructure t)
    ((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)) n₁

Tactic:
infer_instance
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
obtain :
  ∀
    (e :
      T ≅
        Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
          (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
          (Functor.obj
              (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h :
                P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
              (FullSubcategory.mk (P := P) T.obj₂ h₂) :
            Triangle.{v_1, u_1} P.FullSubcategory)),
    e.hom.hom₂ = Iso.hom (Iso.refl T.obj₂) → P T.obj₁ ∧ P T.obj₃
⊢ P T.obj₁ ∧ P T.obj₃

Tactic:
obtain ⟨e, _⟩ := t.triangle_iso_exists hT
    (P.ι.map_distinguished _ ((P.tStructure t).triangleLEGE_distinguished n₀ n₁ h ⟨_, h₂⟩))
    (Iso.refl _) n₀ n₁ inferInstance inferInstance
      (by dsimp; rw [← P.tStructure_isLE_iff]; infer_instance)
      (by dsimp; rw [← P.tStructure_isGE_iff]; infer_instance)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Triangulated.TStructure.triangle_iso_exists, CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished, CategoryTheory.ObjectProperty.ι, inferInstance, CategoryTheory.Iso.refl, CategoryTheory.Functor.map_distinguished, CategoryTheory.ObjectProperty.tStructure
-- 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
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
e :
  T ≅
    Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
      (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
      (Functor.obj
          (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h : P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
          (FullSubcategory.mk (P := P) T.obj₂ h₂) :
        Triangle.{v_1, u_1} P.FullSubcategory)
h_1 : e.hom.hom₂ = Iso.hom (Iso.refl T.obj₂)
⊢ P T.obj₁ ∧ P T.obj₃

Tactic:
exact ⟨(P.prop_iff_of_iso (Triangle.π₁.mapIso e)).2 (P.prop_ι_obj _),
    (P.prop_iff_of_iso (Triangle.π₃.mapIso e)).2 (P.prop_ι_obj _)⟩
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
dsimp : t.IsLE ((t.truncLE n).obj X) n
⊢ t.IsLE ((t.triangleLEGE n (n + 1) ⋯).obj X).obj₁ n

Tactic:
dsimp
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsLE ((t.truncLE n).obj X) n

Tactic:
infer_instance
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
dsimp : t.IsGE ((t.truncGE (n + 1)).obj X) (n + 1)
⊢ t.IsGE ((t.triangleLEGE n (n + 1) ⋯).obj X).obj₃ (n + 1)

Tactic:
dsimp
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsGE ((t.truncGE (n + 1)).obj X) (n + 1)

Tactic:
infer_instance
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ n - 1 + 1 = n

Tactic:
lia
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
dsimp : t.IsLE ((t.truncLE (n - 1)).obj X) (n - 1)
⊢ t.IsLE ((t.triangleLEGE (n - 1) n ⋯).obj X).obj₁ (n - 1)

Tactic:
dsimp
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsLE ((t.truncLE (n - 1)).obj X) (n - 1)

Tactic:
infer_instance
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
dsimp : t.IsGE ((t.truncGE n).obj X) n
⊢ t.IsGE ((t.triangleLEGE (n - 1) n ⋯).obj X).obj₃ n

Tactic:
dsimp
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsGE ((t.truncGE n).obj X) n

Tactic:
infer_instance
-- 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_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ (P ⊓ P') ((t.truncLE n).obj X) ∧ (P ⊓ P') ((t.truncGE n).obj X)

Tactic:
exact
      ⟨⟨(P.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished n _ rfl X) n _ rfl
          (by dsimp; infer_instance) hX (by dsimp; infer_instance)).1,
        (P'.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished n _ rfl X) n _ rfl
          (by dsimp; infer_instance) hX' (by dsimp; infer_instance)).1⟩,
          ⟨(P.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished (n - 1) n (by lia) X)
          (n - 1) n (by lia) (by dsimp; infer_instance) hX (by dsimp; infer_instance)).2,
        (P'.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished (n - 1) n (by lia) X)
          (n - 1) n (by lia) (by dsimp; infer_instance) hX' (by dsimp; infer_instance)).2⟩⟩
-- 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 : IsTriangulated.{v_1, u_1} C
X : C
a : ℤ
h : t.IsGE X a
n : ℤ
⊢ t.plus ((t.truncLE n).obj X) ∧ t.plus ((t.truncGE n).obj X)

Tactic:
⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩

Premises used: inferInstance, And.intro, Exists.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 : IsTriangulated.{v_1, u_1} C
X : C
a : ℤ
h : t.IsGE X a
n : ℤ
⊢ t.plus ((t.truncLE n).obj X) ∧ t.plus ((t.truncGE n).obj X)

Tactic:
exact ⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩
-- 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 : IsTriangulated.{v_1, u_1} C
X : C
a : ℤ
h : t.IsLE X a
n : ℤ
⊢ t.minus ((t.truncLE n).obj X) ∧ t.minus ((t.truncGE n).obj X)

Tactic:
⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩

Premises used: inferInstance, And.intro, Exists.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 : IsTriangulated.{v_1, u_1} C
X : C
a : ℤ
h : t.IsLE X a
n : ℤ
⊢ t.minus ((t.truncLE n).obj X) ∧ t.minus ((t.truncGE n).obj X)

Tactic:
exact ⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩
-- 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 : IsTriangulated.{v_1, u_1} C
⊢ (t.plus ⊓ t.minus).HasInducedTStructure t

Tactic:
infer_instance
-- 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
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
w :
  ∀ (x : C),
    NatTrans.app (t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) ⋯) ≫ t.ω₁δ a' b' c' hab' hbc') x =
      NatTrans.app
        (t.ω₁δ a b c hab hbc ≫
          Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C (A := ℤ) 1))
        x
⊢ t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) ⋯) ≫ t.ω₁δ a' b' c' hab' hbc' =
    t.ω₁δ a b c hab hbc ≫ Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C (A := ℤ) 1)

Tactic:
ext