mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
          (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
dsimp

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map (𝟙 (F.obj ((shiftFunctor C a).obj X))) ≫
          (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ X✝.rotate.mor₃ ≫ (shiftFunctor C 1).map f.hom₂ = (shiftFunctor C 1).map f.hom₁ ≫ Y✝.rotate.mor₃

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C 1).map X✝.mor₁) ≫ (shiftFunctor C 1).map f.hom₂ =
    (shiftFunctor C 1).map f.hom₁ ≫ (-(shiftFunctor C 1).map Y✝.mor₁)
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ X✝.invRotate.mor₁ ≫ f.hom₁ = (shiftFunctor C (-1)).map f.hom₃ ≫ Y✝.invRotate.mor₁

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X✝.obj₁) ≫ f.hom₁ =
    (shiftFunctor C (-1)).map f.hom₃ ≫
      (-(shiftFunctor C (-1)).map Y✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁)
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ X✝.invRotate.mor₁ ≫ f.hom₁ = (shiftFunctor C (-1)).map f.hom₃ ≫ Y✝.invRotate.mor₁

Tactic:
dsimp
      simp only [comp_neg, ← Functor.map_comp_assoc, ← f.comm₃]
      rw [Functor.map_comp]
      simp

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 M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' ⋯).v p q hpq
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
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
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).rightShift a m' hm').v p q hpq

Tactic:
dsimp

Goal state after:
case pos
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
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} E
inst✝¹² : Category.{v_4, u_4} J
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : D ⥤ E
τ'' : G ⟶ G'
H : E ⥤ J
A : Type u_5
inst✝¹¹ : AddMonoid A
inst✝¹⁰ : HasShift C A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
inst✝⁷ : HasShift J A
inst✝⁶ : F₁.CommShift A
inst✝⁵ : F₂.CommShift A
inst✝⁴ : F₃.CommShift A
inst✝³ : G.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : H.CommShift A
inst✝ : CommShift e.hom A
a : A
X : C
⊢ ((Functor.commShiftIso F₂ a).hom ≫ Functor.whiskerRight e.inv (shiftFunctor D a)).app X =
    ((shiftFunctor C a).whiskerLeft e.inv ≫ (Functor.commShiftIso F₁ a).hom).app X

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} E
inst✝¹² : Category.{v_4, u_4} J
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : D ⥤ E
τ'' : G ⟶ G'
H : E ⥤ J
A : Type u_5
inst✝¹¹ : AddMonoid A
inst✝¹⁰ : HasShift C A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
inst✝⁷ : HasShift J A
inst✝⁶ : F₁.CommShift A
inst✝⁵ : F₂.CommShift A
inst✝⁴ : F₃.CommShift A
inst✝³ : G.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : H.CommShift A
inst✝ : CommShift e.hom A
a : A
X : C
⊢ (Functor.commShiftIso F₂ a).hom.app X ≫ (shiftFunctor D a).map (e.inv.app X) =
    e.inv.app ((shiftFunctor C a).obj X) ≫ (Functor.commShiftIso F₁ a).hom.app X
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
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫ (productTriangle T).mor₃

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫
      (Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)
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' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m (((rightShiftAddEquiv K L n a n' hn) γ').rightUnshift n hn) =
    a.negOnePow • (δ n' m' ((rightShiftAddEquiv K L n a n' hn) γ')).rightUnshift m hm'

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ (productTriangle T).mor₃ ≫ (shiftFunctor C 1).map (productTriangle T).mor₁ = 0

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁)) ≫
      (shiftFunctor C 1).map (Limits.Pi.map fun j ↦ (T j).mor₁) =
    0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
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
⊢ (δ n' m' (γ.leftShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).leftShift a m' hm').v p q hpq

Tactic:
dsimp

Goal state after:
case pos
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
⊢ (δ n' m' (γ.leftShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).leftShift a m' hm').v p q hpq
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:
dsimp

Goal state after:
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✝
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁) ≫ (CategoryTheory.shiftFunctor C n).map f.hom₂ =
    (CategoryTheory.shiftFunctor C n).map f.hom₁ ≫ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.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
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:
dsimp

Goal state after:
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✝
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂) ≫ (CategoryTheory.shiftFunctor C n).map f.hom₃ =
    (CategoryTheory.shiftFunctor C n).map f.hom₂ ≫ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.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
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:
dsimp

Goal state after:
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✝
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    (CategoryTheory.shiftFunctor C n).map f.hom₃ ≫
      (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)
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:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
T : Triangle C
⊢ (1 • (CategoryTheory.shiftFunctor C 0).map T.mor₃ ≫ (shiftFunctorComm C 1 0).hom.app T.obj₁) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorZero C ℤ).hom.app T.obj₁) =
    (CategoryTheory.shiftFunctorZero C ℤ).hom.app T.obj₃ ≫ 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 : ℤ
T : Triangle C
⊢ ((shiftFunctor C (a + b)).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₁).hom ≫
      ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₁

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ ((a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₁) ≫
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
      (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map 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 : ℤ
T : Triangle C
⊢ ((shiftFunctor C (a + b)).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₂).hom ≫
      ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₂

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ ((a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₂) ≫
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
      (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map 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 : ℤ
T : Triangle C
⊢ ((shiftFunctor C (a + b)).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₃).hom ≫
      ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₃

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ ((a + b).negOnePow •
        (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
      (b.negOnePow •
        (CategoryTheory.shiftFunctor C b).map
            (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁))
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:
dsimp

Goal state after:
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
⊢ h ≫ (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X) =
    𝟙 Z ≫ h ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj X)
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' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m (((leftShiftAddEquiv K L n a n' hn) γ').leftUnshift n hn) =
    a.negOnePow • (δ n' m' ((leftShiftAddEquiv K L n a n' hn) γ')).leftUnshift m hm'

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
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
⊢ (δ n m (γ.shift a)).v p q hpq = (a.negOnePow • (δ n m γ).shift a).v p q hpq

Tactic:
dsimp

Goal state after:
case pos
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
⊢ (δ n m (γ.shift a)).v p q hpq = a.negOnePow • ((δ n m γ).shift a).v p q hpq
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
⊢ (a * n + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯

Tactic:
dsimp

Goal state after:
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
⊢ (a * n + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯ ≫ 𝟙 (L.X (q + a)) =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
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:
dsimp

Goal state after:
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₃
⊢ (-(shiftFunctor C (-1)).map T₁.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₁.obj₁) ≫ a =
    (shiftFunctor C (-1)).map c ≫
      (-(shiftFunctor C (-1)).map T₂.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₂.obj₁)