mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
inst✝ : t.IsGE Y n
⊢ n - 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ (n✝ + 1) ⋯ = f n✝
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f (n✝ + 1) (n✝ + 1 + 1) ⋯ = f (n✝ + 1)

Tactic:
intro X f
      apply hi

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} D₁
inst✝¹⁰ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : IsTriangulated C
inst✝³ : A.IsTriangulated
inst✝² : B.IsTriangulated
inst✝¹ : B.IsClosedUnderIsomorphisms
inst✝ : A.IsVerdierLeftLocalizing B
⊢ (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
inst✝ : t.IsGE Y n
⊢ t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ map f i (i + 1) ⋯ = f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
h₀ : Homotopy (𝟙 (mappingCone (𝟙 (I K)))) 0 :=
  mappingCone.liftHomotopy (𝟙 (I K)) (𝟙 (mappingCone (𝟙 (I K)))) 0 (mappingCone.snd (𝟙 (I K))) 0 ⋯ ⋯
h₁ : Homotopy (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.fst ≫ 0 ≫ biprod.inl) :=
  (h₀.compRight biprod.inl).compLeft biprod.fst
h₂ : Homotopy (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl + biprod.snd ≫ biprod.inr)
  (biprod.fst ≫ 0 ≫ biprod.inl + biprod.snd ≫ biprod.inr) :=
  h₁.add (Homotopy.refl (biprod.snd ≫ biprod.inr))
⊢ biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (mappingCone (𝟙 (I K)) ⊞ L)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
x✝¹ : t.IsLE X n₀
Y : C
f : X ⟶ Y
x✝ : t.IsGE Y n₁
⊢ n₀ < n₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
⊢ biprod.inr ≫ p K L = 𝟙 L

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
⊢ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).IsStrictlyGE n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
⊢ cm5b.i f ≫ cm5b.p K L = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
⊢ (t.truncGEπ n₁).app X ≫ 𝟙 ((t.truncGE n₁).obj X) = (t.truncGEπ n₁).app X ≫ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁹ : Category.{v_1, u_1} C
inst✝¹⁸ : Category.{v_2, u_2} D
inst✝¹⁷ : Category.{v_3, u_3} D₁
inst✝¹⁶ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹⁵ : HasZeroObject C
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹¹ : Pretriangulated C
inst✝¹⁰ : IsTriangulated C
inst✝⁹ : A.IsTriangulated
inst✝⁸ : B.IsTriangulated
inst✝⁷ : B.IsClosedUnderIsomorphisms
inst✝⁶ : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝⁵ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝⁴ : L₂.IsLocalization B.trW
inst✝³ : Preadditive D₁
inst✝² : Preadditive D₂
inst✝¹ : L₁.Additive
inst✝ : L₂.Additive
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ 0 + 1
⊢ j = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
x✝¹ : t.IsGE X n₁
Y : C
f : Y ⟶ X
x✝ : t.IsLE Y n₀
⊢ n₀ < n₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ t.IsLE ((t.truncLT n₁).obj X) n₀

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ 𝟙 ((t.truncLT n₁).obj X) ≫ (t.truncLTι n₁).app X = 0 ≫ (t.truncLTι n₁).app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ 0 ≤ j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ j ≤ k + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
Y : C
f : T.obj₂ ⟶ Y
hY : t.IsGE Y (n + 1)
⊢ n < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
Y : C
f : T.obj₂ ⟶ Y
hY : t.IsGE Y (n + 1)
f' : T.obj₃ ⟶ Y
hf' : f = T.mor₂ ≫ f'
⊢ n < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
⊢ t.IsLE T.obj₂ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
⊢ n - 1 + 1 = n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
Y : C
f : Y ⟶ T.obj₂
hY : t.IsLE Y (n - 1)
⊢ n - 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
Y : C
f : Y ⟶ T.obj₂
hY : t.IsLE Y (n - 1)
f' : Y ⟶ T.obj₁
hf' : f = f' ≫ T.mor₁
⊢ n - 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
⊢ t.IsGE T.obj₂ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
hij : i + 1 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1
⊢ i ≤ j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ t.minus T.obj₁ → t.minus T.obj₃ → t.minus T.obj₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j : ℕ
hij : i + 1 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1
⊢ j ≤ k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ t.plus T.obj₁ → t.plus T.obj₃ → t.plus T.obj₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j k : ℕ
hij : i ≤ j
hjk : j ≤ k
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
⊢ t.bounded.IsTriangulated

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ 5 ≤ 5

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ 0 ≤ 3

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ 3 ≤ 7

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
i j : ℕ
φ : i ⟶ j
k : ℕ
hk : j = i + k
⊢ i ≤ j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
i j : ℕ
hk : j = i + 0
⊢ j = i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsLE (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₁ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
k : ℕ
hk :
  ∀ ⦃i j : ℕ⦄ (hk : j = i + k),
    F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk)) ≫ app j =
      app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk))
i j : ℕ
hk' : j = i + (k + 1)
⊢ j = i + k + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsGE (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₃ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsLE ((t.triangleLTGE n).obj Y).obj₁ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsGE ((t.triangleLTGE n).obj Y).obj₃ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
⊢ ∀ ⦃X Y : ℕ⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
n : ℕ
⊢ (ofOpSequence f).map (homOfLE ⋯).op = f n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕᵒᵖ ⥤ C
app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n)
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯).op ≫ app n = app (n + 1) ≫ G.map (homOfLE ⋯).op
x✝¹ x✝ : ℕᵒᵖ
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ app (Opposite.unop x✝) = app (Opposite.unop x✝¹) ≫ G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
this : (t.truncLT n).map f = e.hom.hom₁
⊢ IsIso ((t.truncLT n).map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
⊢ (t.truncLT n).map f ≫ (t.truncLTι n).app Y = (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).mor₁ ≫ e.hom.hom₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
⊢ IsIso ((t.truncLT n).map f) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ t.IsLE ((t.truncLT n₁).obj Y) n₀

Tactic:
by

Goal state after: