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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
X : C
⊢ (zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
by

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).hom =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
                (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
                  ((shiftFunctor C a).associator F (s b)).symm ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom.app
      X =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
by

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
a b : A
X : C
⊢ (add F s i a b).hom.app (F.obj X) =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
by

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
                (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
                  ((shiftFunctor C a).associator F (s b)).symm ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv.app
      X =
    (s b).map ((i a).hom.app 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:
by

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
a b : A
X : C
⊢ (add F s i a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app 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:
by

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
m₁ m₂ m₃ : A
⊢ s (m₁ + m₂ + m₃) = s (m₁ + (m₂ + m₃))

Tactic:
by

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
m₁ m₂ m₃ : A
this :
  (Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
⊢ ∀ (X : D),
    (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ LiftCommShift.iso F r hF 0 = Functor.CommShift.isoZero (lift r F hF) A

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
⊢ n.negOnePow • K.d (i + n) (j + n) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
⊢ ∀ (i j k : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (ComplexShape.up ℤ).Rel j k → (n.negOnePow • K.d (i + n) (j + n)) ≫ (n.negOnePow • K.d (j + n) (k + n)) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
X✝ Y✝ : CochainComplex C ℤ
φ : X✝ ⟶ Y✝
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      φ.f (i + n) ≫
          { X := fun i ↦ Y✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • Y✝.d (x + n) (x_1 + n), shape := ⋯,
                d_comp_d' := ⋯ }.d
            i j =
        { X := fun i ↦ X✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • X✝.d (x + n) (x_1 + n), shape := ⋯,
                d_comp_d' := ⋯ }.d
            i j ≫
          φ.f (j + n)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
⊢ ∀ (X : CochainComplex C ℤ),
    { f := fun x ↦ (𝟙 X).f (x + n), comm' := ⋯ } =
      𝟙 { X := fun i ↦ X.X (i + n), d := fun x x_1 ↦ n.negOnePow • X.d (x + n) (x_1 + n), shape := ⋯, d_comp_d' := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
⊢ ∀ {X Y Z : CochainComplex C ℤ} (f : X ⟶ Y) (g : Y ⟶ Z),
    { f := fun x ↦ (f ≫ g).f (x + n), comm' := ⋯ } =
      { f := fun x ↦ f.f (x + n), comm' := ⋯ } ≫ { f := fun x ↦ g.f (x + n), comm' := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
h : n = 0
K : CochainComplex C ℤ
i : ℤ
⊢ i = i + n

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
h : n = 0
K : CochainComplex C ℤ
x✝² x✝¹ : ℤ
x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹
⊢ (K.shiftFunctorObjXIso n x✝² x✝² ⋯).hom ≫ ((𝟭 (CochainComplex C ℤ)).obj K).d x✝² x✝¹ =
    ((shiftFunctor C n).obj K).d x✝² x✝¹ ≫ (K.shiftFunctorObjXIso n x✝¹ x✝¹ ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
h : n = 0
X✝ Y✝ : CochainComplex C ℤ
x✝ : X✝ ⟶ Y✝
⊢ (shiftFunctor C n).map x✝ ≫ (Hom.isoOfComponents (fun i ↦ Y✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ X✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom ≫ (𝟭 (CochainComplex C ℤ)).map x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex C ℤ
i : ℤ
⊢ i + n₂ + n₁ = i + n₁₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
⊢ LiftCommShift.iso F r hF (a + b) = Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex C ℤ
x✝² x✝¹ : ℤ
x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹
⊢ (K.shiftFunctorObjXIso n₁₂ x✝² (x✝² + n₂ + n₁) ⋯).hom ≫ ((shiftFunctor C n₁ ⋙ shiftFunctor C n₂).obj K).d x✝² x✝¹ =
    ((shiftFunctor C n₁₂).obj K).d x✝² x✝¹ ≫ (K.shiftFunctorObjXIso n₁₂ x✝¹ (x✝¹ + n₂ + n₁) ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
⊢ ∀ {X Y : CochainComplex C ℤ} (f : X ⟶ Y),
    (shiftFunctor C n₁₂).map f ≫ (Hom.isoOfComponents (fun i ↦ Y.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom =
      (Hom.isoOfComponents (fun i ↦ X.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom ≫
        (shiftFunctor C n₁ ⋙ shiftFunctor C n₂).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + { as := b }.as + { as := a }.as = n + { as := a + b }.as

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + { as := a + b }.as = n + { as := b }.as + { as := a }.as

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + { as := b }.as + { as := a }.as = n + { as := ab }.as

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
⊢ (Functor.commShiftIso (functor r ⋙ lift r F hF) a).hom ≫
      Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a) =
    (shiftFunctor C a).whiskerLeft (lift.isLift r F hF).hom ≫ (Functor.commShiftIso F a).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + { as := ab }.as = n + { as := b }.as + { as := a }.as

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n = n + { as := 0 }.as

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n + { as := 0 }.as = n

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b c : ℤ
h : a + b = c
⊢ CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h = shiftFunctorAdd' C a b c h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b : ℤ
⊢ shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
⊢ shiftFunctorZero (CochainComplex C ℤ) ℤ = shiftFunctorZero' C 0 ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b p : ℤ
⊢ p + (b + a) = p + a + b

Tactic:
add_comm b,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b p : ℤ
⊢ p + (a + b) = p + a + b
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (XIsoOfEq K ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n i i' : ℤ
hi : n + i = i'
K : CochainComplex C ℤ
⊢ i + { as := n }.as = i'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n i i' : ℤ
hi : n + i = i'
⊢ ∀ {X Y : CochainComplex C ℤ} (f : X ⟶ Y),
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ eval C (ComplexShape.up ℤ) i).map f ≫ (XIsoOfEq Y ⋯).hom =
      (XIsoOfEq X ⋯).hom ≫ (eval C (ComplexShape.up ℤ) i').map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
K : HomologicalComplex C (ComplexShape.up ℤ)
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    K).X
                i)).hom ≫
          ((F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n).obj
                K).d
            i j =
        ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                K).d
            i j ≫
          (Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    K).X
                j)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
X✝ Y✝ : HomologicalComplex C (ComplexShape.up ℤ)
x✝ : X✝ ⟶ Y✝
⊢ (shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)).map x✝ ≫
      (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦
            Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    Y✝).X
                x))
          ⋯).hom =
    (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦
            Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    X✝).X
                x))
          ⋯).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n).map x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ F.mapCochainComplexShiftIso 0 = CommShift.isoZero (F.mapHomologicalComplex (ComplexShape.up ℤ)) ℤ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
a b : ℤ
⊢ F.mapCochainComplexShiftIso (a + b) = CommShift.isoAdd (F.mapCochainComplexShiftIso a) (F.mapCochainComplexShiftIso b)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
⊢ n.negOnePow • h.hom (i + { as := n }.as) (j + { as := n }.as) = 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 : ℤ
γ γ₁ γ₂ : 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
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
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ p' = 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' : ℤ
hp' : p + n = p'
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a q p' ⋯).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₁).f i =
    (((dNext i) fun x x_1 ↦ n.negOnePow • h.hom (x + { as := n }.as) (x_1 + { as := n }.as)) +
        (prevD i) fun x x_1 ↦ n.negOnePow • h.hom (x + { as := n }.as) (x_1 + { as := n }.as)) +
      ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₂).f i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
⊢ HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ

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 : ℤ
γ γ₁ γ₂ : 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.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive

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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ p' = p + a

Tactic:
by

Goal state after: