mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inl ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd

pp: case h₁.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.fst

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd

Tactic:
·

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inl ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.fst

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd

Tactic:
·

Goal state after:
case h₁.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.fst
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case mpr
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 : ℤ
X : C
⊢ IsIso ((t.truncGEπ n).app X) → t.IsGE X n

Tactic:
·

Goal state after:
case mpr
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 : ℤ
X : C
⊢ IsIso ((t.truncGEπ n).app X) → t.IsGE X n
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd

Tactic:
·

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd
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
⊢ 1 + 1 = 2

Tactic:
by lia

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 : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : (shiftFunctor C 1).obj ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
⊢ n - 2 < n

Tactic:
by lia

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
p q : ℤ
hpq : p + 2 = q
⊢ 1 + 1 = 2

Tactic:
by lia

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
p q : ℤ
hpq : p + 2 = q
⊢ p + 1 = q - 1

Tactic:
by lia

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 : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
hf : (t.truncGEπ n).app X ≫ f = 0
g : (shiftFunctor C 1).obj ((t.triangleLTGE n).obj X).obj₁ ⟶ Y
hg : f = ((t.triangleLTGE n).obj X).mor₃ ≫ g
⊢ 1 + (n - 2) = n - 1

Tactic:
by lia

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 : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
⊢ n - 1 < n + 1

Tactic:
by lia

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 : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
⊢ -1 + (n + 1) = n

Tactic:
by lia

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

Goal state before:
pp: case refine_2
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 ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ (B.op.inverseImage A.op.ι).trW.IsInvertedBy (A.opEquivalence.functor ⋙ L₁.op)

Tactic:
·

Goal state after:
case refine_2
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 ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ (B.op.inverseImage A.op.ι).trW.IsInvertedBy (A.opEquivalence.functor ⋙ L₁.op)
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)
x✝¹ : ℕ → C
f : (n : ℕ) → x✝¹ n ⟶ x✝¹ (n + 1)
l : ℕ
x✝ : 0 ≤ l + 1
⊢ 0 ≤ l

Tactic:
by lia

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)
x✝¹ : ℕ → C
f : (n : ℕ) → x✝¹ n ⟶ x✝¹ (n + 1)
k l : ℕ
x✝ : k + 1 ≤ l + 1
⊢ k ≤ l

Tactic:
by lia

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 : ℕ
⊢ i ≤ i

Tactic:
by lia

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : t.IsLE X n₀
⊢ n₀ < n₁

Tactic:
by lia

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 : ℕ
⊢ i ≤ i + 1

Tactic:
by lia

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
⊢ n - 1 < n

Tactic:
by lia

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 lia

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

Goal state before:
pp: case zero.succ.zero
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
⊢ map f 0 0 ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) 0 hjk

pp: case zero.succ.succ.zero
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
⊢ map f 0 (0 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (0 + 1) hjk

pp: case zero.succ.succ.succ
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
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
·

Goal state after:
case zero.succ.zero
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
⊢ map f 0 0 ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) 0 hjk
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.zero
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
⊢ map f 0 (0 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (0 + 1) hjk

pp: case zero.succ.succ.succ
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
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
·

Goal state after:
case zero.succ.succ.zero
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
⊢ map f 0 (0 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (0 + 1) hjk
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 lia

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 lia

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

Goal state before:
pp: case zero.succ.succ.succ
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
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
·

Goal state after:
case zero.succ.succ.succ
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
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk
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 lia

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 lia

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 lia

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 lia

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 lia

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

Goal state before:
pp: case succ.zero.zero
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)
hij : i + 1 ≤ 0
hjk : 0 ≤ 0
⊢ map f (i + 1) 0 ⋯ = map f (i + 1) 0 hij ≫ map f 0 0 hjk

pp: case succ.zero.succ
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)
hij : i + 1 ≤ 0
k : ℕ
hjk : 0 ≤ k + 1
⊢ map f (i + 1) (k + 1) ⋯ = map f (i + 1) 0 hij ≫ map f 0 (k + 1) hjk

pp: case succ.succ.zero
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
hjk : j + 1 ≤ 0
⊢ map f (i + 1) 0 ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) 0 hjk

pp: case succ.succ.succ
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
⊢ map f (i + 1) (k + 1) ⋯ = map f (i + 1) (j + 1) hij ≫ map f (j + 1) (k + 1) hjk

Tactic:
·

Goal state after:
case succ.zero.zero
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)
hij : i + 1 ≤ 0
hjk : 0 ≤ 0
⊢ map f (i + 1) 0 ⋯ = map f (i + 1) 0 hij ≫ map f 0 0 hjk