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
n : A
X : C
eq : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫ (F ⋙ s n).map ((shiftFunctorZero C A).inv.app X) ≫ (s n).map ((i 0).inv.app X) =
    eqToHom ⋯ ≫ (s n).map (F.map ((shiftFunctorZero C A).inv.app X)) ≫ (s n).map ((i 0).inv.app X)

Tactic:
]

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
n : A
X : C
eq : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫ (F ⋙ s n).map ((shiftFunctorZero C A).inv.app X) ≫ (s n).map ((i 0).inv.app X) =
    eqToHom ⋯ ≫ (s n).map (F.map ((shiftFunctorZero C A).inv.app X)) ≫ (s n).map ((i 0).inv.app X)
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
n : A
⊢ s n = s n ⋙ 𝟭 D

Tactic:
]

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
n : A
⊢ s n = s n ⋙ 𝟭 D
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
⊢ γ.v p q hpq = γ.v p q hpq

Tactic:
]

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'
p q : ℤ
hpq : p + n' = q
⊢ γ.v p q ⋯ = γ.v p q hpq

Tactic:
]

Goal state after:
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
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫
          F.map (eqToHom ⋯ ≫ (shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X)) ≫
            (i 0).inv.app ((shiftFunctor C n).obj X) =
    (eqToHom ⋯).app (F.obj X) ≫
      (𝟭 D).map ((i n).hom.app X) ≫
        F.map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X)) ≫ (i 0).inv.app ((shiftFunctor C n).obj X)

Tactic:
]

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
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫
          F.map (eqToHom ⋯ ≫ (shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X)) ≫
            (i 0).inv.app ((shiftFunctor C n).obj X) =
    (eqToHom ⋯).app (F.obj X) ≫
      (𝟭 D).map ((i n).hom.app X) ≫
        F.map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X)) ≫ (i 0).inv.app ((shiftFunctor C n).obj X)
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
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ CommShift.isoZero F A = CommShift.isoZero F A

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 A.obj₁ = 𝟙 A.obj₁

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 A.obj₂ = 𝟙 A.obj₂

Tactic:
]

Goal state after:
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:
]

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 (𝟙 ((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
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 A.obj₃ = 𝟙 A.obj₃

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 B.obj₁ = 𝟙 B.obj₁

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 B.obj₂ = 𝟙 B.obj₂

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ 𝟙 B.obj₃ = 𝟙 B.obj₃

Tactic:
]

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
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (commShiftIso F (a + b)).hom.app X =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ F.map ((shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) =
    F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (commShiftIso F (a + b)).hom.app X ≫
        (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (commShiftIso F (a + b)).hom.app X =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ F.map ((shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) =
    F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (commShiftIso F (a + b)).hom.app X ≫
        (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)
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 = (i (a + b)).inv.app X

Tactic:
]

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
m a : ℤ
γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom

Tactic:
]

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

Tactic:
]

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 X✝.mor₃ ≫ (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁)) ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁
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
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      F.map ((shiftFunctorAdd' C a b 0 h).inv.app X) ≫ F.map ((shiftFunctorZero C A).hom.app X) =
    F.map ((shiftFunctorZero C A).hom.app X) ≫
      (shiftFunctorZero D A).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      F.map ((shiftFunctorAdd' C a b 0 h).inv.app X) ≫ F.map ((shiftFunctorZero C A).hom.app X) =
    F.map ((shiftFunctorZero C A).hom.app X) ≫
      (shiftFunctorZero D A).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)
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 : ℤ
γ γ₁ γ₂ : 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'
⊢ n + (m + a) = n + (m + a)

Tactic:
]

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
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ 𝟙 (F.obj ((shiftFunctor C a ⋙ shiftFunctor C b).obj X)) =
    ((commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) ≫
      (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).inv.app X) ≫ (commShiftIso F b).inv.app ((shiftFunctor C a).obj X)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ 𝟙 (F.obj ((shiftFunctor C a ⋙ shiftFunctor C b).obj X)) =
    ((commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) ≫
      (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).inv.app X) ≫ (commShiftIso F b).inv.app ((shiftFunctor C a).obj X)
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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
⊢ (shiftFunctor D a).map (τ.app X) = (shiftFunctor D a).map (τ.app X)

Tactic:
]

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

Goal state before:
pp: case e_a.e_a
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'
⊢ (a * m).negOnePow * (a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow

Tactic:
]

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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
⊢ ((Functor.commShiftIso F₁ (a + b)).hom ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))).app X =
    ((shiftFunctor C (a + b)).whiskerLeft τ ≫ (Functor.commShiftIso F₂ (a + b)).hom).app X

Tactic:
have := (shiftFunctorAdd D a b).inv.naturality (τ.app X)

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  (shiftFunctor D a ⋙ shiftFunctor D b).map (τ.app X) ≫ (shiftFunctorAdd D a b).inv.app (F₂.obj X) =
    (shiftFunctorAdd D a b).inv.app (F₁.obj X) ≫ (shiftFunctor D (a + b)).map (τ.app X)
⊢ ((Functor.commShiftIso F₁ (a + b)).hom ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))).app X =
    ((shiftFunctor C (a + b)).whiskerLeft τ ≫ (Functor.commShiftIso F₂ (a + b)).hom).app X
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'
γ' : Cochain L M 0
⊢ (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯

Tactic:
]

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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F₁.CommShift A
inst✝¹ : F₂.CommShift A
inst✝ : CommShift τ A
a : A
X : C
⊢ (shiftFunctor D a).map (τ.app X) = (shiftFunctor D a).map (τ.app X)

Tactic:
]

Goal state after:
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
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L).d (p + n') q +
      m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + m) ⋯).inv =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv

Tactic:
]

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
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L).d (p + n') q +
      m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + m) ⋯).inv =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv
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₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫ Limits.Pi.map fun j ↦ (T j).mor₃

Tactic:
]

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₁) ≫ piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫ Limits.Pi.map fun j ↦ (T j).mor₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case neg
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'
⊢ 0 = 0

Tactic:
]

Goal state after:
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.app X = (Functor.commShiftIso F₁ a).hom.app X

Tactic:
]

Goal state after:
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₂
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫
      inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
        (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) ≫
          piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) =
    0

Tactic:
]

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 (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) ≫
          piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) =
    0