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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((rotate C ⋙ rotate C ⋙ rotate C).obj T).mor₂ ≫ (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₃).hom =
    (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₂).hom ≫ ((Triangle.shiftFunctor C 1).obj T).mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((rotate C ⋙ rotate C ⋙ rotate C).obj T).mor₃ ≫
      (shiftFunctor C 1).map (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₁).hom =
    (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₃).hom ≫ ((Triangle.shiftFunctor C 1).obj T).mor₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ p + a + n' = q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (rotate C ⋙ rotate C ⋙ rotate C).map f ≫
        (((rotate C ⋙ rotate C ⋙ rotate C).obj Y).isoMk ((Triangle.shiftFunctor C 1).obj Y)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj Y).obj₁)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj Y).obj₂)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((rotate C ⋙ rotate C ⋙ rotate C).obj X).isoMk ((Triangle.shiftFunctor C 1).obj X)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj X).obj₁)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj X).obj₂)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (Triangle.shiftFunctor C 1).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ p + a + n = q + a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).mor₁ ≫
      (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₂).hom =
    (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₁).hom ≫ ((Triangle.shiftFunctor C (-1)).obj T).mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).mor₂ ≫
      (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₃).hom =
    (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₂).hom ≫ ((Triangle.shiftFunctor C (-1)).obj T).mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).mor₃ ≫
      (shiftFunctor C 1).map (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₁).hom =
    (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₃).hom ≫ ((Triangle.shiftFunctor C (-1)).obj T).mor₃

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (invRotate C ⋙ invRotate C ⋙ invRotate C).map f ≫
        (((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).isoMk ((Triangle.shiftFunctor C (-1)).obj Y)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).obj₁)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).obj₂)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).isoMk ((Triangle.shiftFunctor C (-1)).obj X)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).obj₁)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).obj₂)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (Triangle.shiftFunctor C (-1)).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ T₁.invRotate.mor₁ ≫ a = (shiftFunctor C (-1)).map c ≫ T₂.invRotate.mor₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ p + n' = q + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ p + a + n = q + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom =
    (shiftFunctor C (-1)).mapZeroObject.symm.hom ≫ (contractibleTriangle X).invRotate.mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T ≫
      (shiftFunctor C c).map ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app T) =
    eqToHom ⋯ ≫
      (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯).hom.app T ≫
        (shiftFunctorAdd' C b c (b + c) ⋯).hom.app ((shiftFunctor C a).obj T)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₂ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom ≫ (contractibleTriangle X).invRotate.mor₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n' + a = n
⊢ n' + 1 + a = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n' + a = n
⊢ δ n' (n' + 1) ((↑γ).rightShift a n' hn') = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₃ ≫ (shiftFunctor C 1).map (shiftFunctor C (-1)).mapZeroObject.symm.hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom ≫ (contractibleTriangle X).invRotate.mor₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ n + 1 - a + a = n + 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ∈ distinguishedTriangles

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ δ n (n + 1) ((↑γ).rightUnshift n hn) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
h : a + b = c
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h = shiftFunctorAdd' C a b c h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n + a = n'
⊢ n + 1 + a = n' + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cocycle K L n
a n' : ℤ
hn' : n + a = n'
⊢ δ n' (n' + 1) ((↑γ).leftShift a n' hn') = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₁ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate.mor₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ δ n (n + 1) ((↑γ).leftUnshift n hn) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cocycle K L n
a : ℤ
⊢ δ n (n + 1) ((↑γ).shift a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n' + a = n
γ : Cocycle K L n
⊢ (fun γ ↦ γ.rightUnshift n hn') ((fun γ ↦ γ.rightShift a n' hn') γ) = γ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₂ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom ≫
      (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate.mor₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n' + a = n
γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
⊢ (fun γ ↦ γ.rightShift a n' hn') ((fun γ ↦ γ.rightUnshift n hn') γ) = γ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n' + a = n
γ γ' : Cocycle K L n
⊢ (γ + γ').rightShift a n' hn' = γ.rightShift a n' hn' + γ'.rightShift a n' hn'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
K' : CochainComplex C ℤ
g : K' ⟶ K
f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
⊢ equivHomShift (g ≫ f) = (equivHomShift f).precomp g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
K' : CochainComplex C ℤ
g : K' ⟶ K
⊢ equivHomShift (equivHomShift.symm (z.precomp g)) = equivHomShift (g ≫ equivHomShift.symm z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
L' : CochainComplex C ℤ
g : L ⟶ L'
⊢ equivHomShift (f ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map g) = (equivHomShift f).postcomp g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₃ ≫ (shiftFunctor C 1).map ((shiftEquiv C 1).unitIso.app X).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom ≫
      (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate.mor₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
L' : CochainComplex C ℤ
g : L ⟶ L'
⊢ equivHomShift (equivHomShift.symm (z.postcomp g)) =
    equivHomShift (equivHomShift.symm z ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n + a = n'
γ : Cocycle K L n
⊢ (fun γ ↦ γ.leftUnshift n hn') ((fun γ ↦ γ.leftShift a n' hn') γ) = γ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n + a = n'
γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
⊢ (fun γ ↦ γ.leftShift a n' hn') ((fun γ ↦ γ.leftUnshift n hn') γ) = γ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n + a = n'
γ γ' : Cocycle K L n
⊢ (γ + γ').leftShift a n' hn' = γ.leftShift a n' hn' + γ'.leftShift a n' hn'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ T.mor₁ ≫ f = 0 ≫ (mk 0 (𝟙 X) 0).mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃
⊢ f = T.mor₂ ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ ∃ g, f = T.mor₂ ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ (contractibleTriangle X).mor₂ ≫ 0 = f ≫ T.mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ f = a ≫ T.mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ ∃ g, f = g ≫ T.mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ (CategoryTheory.shiftFunctor C 1).obj T.obj₁
hf : f ≫ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
⊢ f ≫ T.rotate.rotate.mor₂ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₁ ≅ (contractibleTriangle 0).obj₁

Tactic:
by

Goal state after: