mathlib-initiative/mathlib-tactics huggingface dataset:
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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + a + n = p + n'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
A : Type u_4
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a : A
⊢ commShiftIso F a = i 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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + 1 + n' = q

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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + 1 + a + n = q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
⊢ G.map ((iso e a).hom.app X) =
    e.hom.app ((shiftFunctor C a).obj X) ≫
      (commShiftIso H a).hom.app X ≫ (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)

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
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂)
          (n.negOnePow •
            (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁)).mor₁ ≫
      (CategoryTheory.shiftFunctor C n).map f.hom₂ =
    (CategoryTheory.shiftFunctor C n).map f.hom₁ ≫
      (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)).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
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂)
          (n.negOnePow •
            (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁)).mor₂ ≫
      (CategoryTheory.shiftFunctor C n).map f.hom₃ =
    (CategoryTheory.shiftFunctor C n).map f.hom₂ ≫
      (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)).mor₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
⊢ G.map ((iso e a).inv.app X) =
    (commShiftIso G a).hom.app (F.obj X) ≫
      (shiftFunctor E a).map (e.hom.app X) ≫ (commShiftIso H a).inv.app X ≫ e.inv.app ((shiftFunctor C a).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x✝¹ x✝ : J
φ : x✝¹ ⟶ x✝
⊢ A.map φ ≫ { hom₁ := hom₁.app x✝, hom₂ := hom₂.app x✝, hom₃ := hom₃.app x✝, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ } =
    { hom₁ := hom₁.app x✝¹, hom₂ := hom₂.app x✝¹, hom₃ := hom₃.app x✝¹, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ } ≫ B.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
⊢ OfComp.iso e 0 = isoZero F 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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂)
          (n.negOnePow •
            (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁)).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    (CategoryTheory.shiftFunctor C n).map f.hom₃ ≫
      (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)).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
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₁).hom ≫ ((𝟭 (Triangle C)).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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₂).hom ≫ ((𝟭 (Triangle C)).obj T).mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₁Toπ₂ ≫ iso₂.inv = iso₁.inv ≫ A.whiskerLeft π₁Toπ₂

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
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₃).hom ≫ ((𝟭 (Triangle C)).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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (shiftFunctor C 0).map f ≫
        (((shiftFunctor C 0).obj Y).isoMk ((𝟭 (Triangle C)).obj Y) ((CategoryTheory.shiftFunctorZero C ℤ).app Y.obj₁)
            ((CategoryTheory.shiftFunctorZero C ℤ).app Y.obj₂) ((CategoryTheory.shiftFunctorZero C ℤ).app Y.obj₃) ⋯ ⋯
            ⋯).hom =
      (((shiftFunctor C 0).obj X).isoMk ((𝟭 (Triangle C)).obj X) ((CategoryTheory.shiftFunctorZero C ℤ).app X.obj₁)
            ((CategoryTheory.shiftFunctorZero C ℤ).app X.obj₂) ((CategoryTheory.shiftFunctorZero C ℤ).app X.obj₃) ⋯ ⋯
            ⋯).hom ≫
        (𝟭 (Triangle C)).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₂Toπ₃ ≫ iso₃.inv = iso₂.inv ≫ A.whiskerLeft π₂Toπ₃

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.inv (shiftFunctor C 1) = iso₃.inv ≫ A.whiskerLeft π₃Toπ₁

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 n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
⊢ OfComp.iso e (a + b) = isoAdd (OfComp.iso e a) (OfComp.iso e b)

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 : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₁ ≫ T.mor₂ = 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
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 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
Y Z : C
g : Y ⟶ Z
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
⊢ NatTrans.CommShift e.hom 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
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₁ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.mk h f' g').invRotate.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 n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₂).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).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 n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : ¬n + 1 = m
x✝ : n' + 1 = m'
⊢ n + 1 = m

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
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₂ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom ≫
      (Triangle.mk h f' g').invRotate.invRotate.mor₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝²⁵ : Category.{v_1, u_1} C₁
inst✝²⁴ : Category.{v_2, u_2} C₂
inst✝²³ : Category.{v_3, u_3} C₃
inst✝²² : Category.{v_4, u_4} D₁
inst✝²¹ : Category.{v_5, u_5} D₂
inst✝²⁰ : Category.{v_6, u_6} D₃
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : D₁ ⥤ D₂
G₂₃ : D₂ ⥤ D₃
G₁₃ : D₁ ⥤ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃
A : Type u_7
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : HasShift C₁ A
inst✝¹⁷ : HasShift C₂ A
inst✝¹⁶ : HasShift C₃ A
inst✝¹⁵ : HasShift D₁ A
inst✝¹⁴ : HasShift D₂ A
inst✝¹³ : HasShift D₃ A
inst✝¹² : F₁₂.CommShift A
inst✝¹¹ : F₂₃.CommShift A
inst✝¹⁰ : F₁₃.CommShift A
inst✝⁹ : CommShift α A
inst✝⁸ : G₁₂.CommShift A
inst✝⁷ : G₂₃.CommShift A
inst✝⁶ : G₁₃.CommShift A
inst✝⁵ : CommShift β A
inst✝⁴ : L₁.CommShift A
inst✝³ : L₂.CommShift A
inst✝² : L₃.CommShift A
inst✝¹ : CommShift e₁₂ A
inst✝ : CommShift e₂₃ A
h₁₃ :
  e₁₃ =
    Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β
⊢ CommShift e₁₃ 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
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₃ ≫
      (shiftFunctor C 1).map ((shiftEquiv C 1).unitIso.app X).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom ≫
      (Triangle.mk h f' g').invRotate.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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

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
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
⊢ ∃ Y f g, Triangle.mk f g h ∈ 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
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
⊢ δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'

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 n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).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 : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ p + a + m = 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 m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ q - 1 + a = q + a - 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
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ p + a + 1 = p + 1 + a

Tactic:
by

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

Goal state before:
pp: case refine_1
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₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : -(shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (-(shiftFunctor C 1).map T₂.mor₁)
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)

Tactic:
comp_neg,

Goal state after:
case refine_1
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₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : -(shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = -a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
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 n : ℤ
h : a + b = n
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (shiftFunctor C n).map f ≫
        (((shiftFunctor C n).obj Y).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y.obj₃) ⋯ ⋯ ⋯).hom =
      (((shiftFunctor C n).obj X).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f

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₁ ≫ (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: