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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : C
⊢ (shiftFunctor C c).map ((↑(t.z a b)).app X) = (↑(t.z a b)).app ((shiftFunctor C c).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b : A
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (shiftFunctor C (a + b)).map f ≫ (t.z a b • (shiftFunctorAdd C a b).app Y).hom =
      (t.z a b • (shiftFunctorAdd C a b).app X).hom ≫ (shiftFunctor C a ⋙ shiftFunctor C b).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (NatIso.ofComponents (fun X ↦ t.z (a + b) c • (shiftFunctorAdd C (a + b) c).app X) ⋯).hom.app X ≫
      (shiftFunctor C c).map ((NatIso.ofComponents (fun X ↦ t.z a b • (shiftFunctorAdd C a b).app X) ⋯).hom.app X) =
    eqToHom ⋯ ≫
      (NatIso.ofComponents (fun X ↦ t.z a (b + c) • (shiftFunctorAdd C a (b + c)).app X) ⋯).hom.app X ≫
        (NatIso.ofComponents (fun X ↦ t.z b c • (shiftFunctorAdd C b c).app X) ⋯).hom.app ((shiftFunctor C a).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
⊢ ∀ (n : A) (X : t.Category),
    (NatIso.ofComponents (fun X ↦ t.z 0 n • (shiftFunctorAdd C 0 n).app X) ⋯).hom.app X =
      eqToHom ⋯ ≫ (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
⊢ ∀ (n : A) (X : t.Category),
    (NatIso.ofComponents (fun X ↦ t.z n 0 • (shiftFunctorAdd C n 0).app X) ⋯).hom.app X =
      eqToHom ⋯ ≫ (shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
X Y : t.Category
f : X ⟶ Y
m : A
⊢ (shiftFunctor t.Category m).map f = (t.shiftIso m).hom.app X ≫ (shiftFunctor C m).map f ≫ (t.shiftIso m).inv.app Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).hom.app X =
    ↑(t.z i j) •
      (t.shiftIso k).hom.app X ≫
        (shiftFunctorAdd' C i j k h).hom.app X ≫
          (shiftFunctor C j).map ((t.shiftIso i).inv.app X) ≫ (t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).inv.app X = ↑(t.z i j)⁻¹ • (shiftFunctorAdd' C i j k h).inv.app X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).inv.app X =
    ↑(t.z i j)⁻¹ •
      (t.shiftIso j).hom.app ((shiftFunctor t.Category i).obj X) ≫
        (shiftFunctor C j).map ((t.shiftIso i).hom.app X) ≫
          (shiftFunctorAdd' C i j k h).inv.app X ≫ (t.shiftIso k).inv.app X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.π c₂ c (c₁.next i₁, i₂) = c.next j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.π c₂ c (c₁.prev i₁, i₂) = c.prev j

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝³ : Category.{v_5, u_5} D
inst✝² : Preadditive D
inst✝¹ : HasShift D ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
x✝² x✝¹ x✝ : ℤ × ℤ
⊢ (-1) ^ ((x✝² + x✝¹).1 * x✝.2) * (-1) ^ (x✝².1 * x✝¹.2) = (-1) ^ (x✝².1 * (x✝¹ + x✝).2) * (-1) ^ (x✝¹.1 * x✝.2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
a x a' : ℤ
h : a' = a + x
b : ℤ
⊢ (((shiftFunctor₁ C x).obj K).X a).X b = (K.X a').X b

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝³ : Category.{v_5, u_5} D
inst✝² : Preadditive D
inst✝¹ : HasShift D ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
x✝¹ x✝ : ℤ × ℤ
⊢ ∀ (a : ℤ × ℤ),
    (Functor.commShiftIso (𝟭 (PullbackShift D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ))) a).hom ≫
        Functor.whiskerRight (↑((-1) ^ (x✝¹.1 * x✝.2)))
          (shiftFunctor (PullbackShift D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)) a) =
      (shiftFunctor (PullbackShift D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)) a).whiskerLeft
          ↑((-1) ^ (x✝¹.1 * x✝.2)) ≫
        (Functor.commShiftIso (𝟭 (PullbackShift D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ))) a).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
a b y b' : ℤ
h : b' = b + y
⊢ (((shiftFunctor₂ C y).obj K).X a).X b = (K.X a).X b'

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' Y₁' : C₁'
f : X₁' ⟶ Y₁'
⊢ NatTrans.CommShift ((F ⋙ G).map f) M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (a + x, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (a - x, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
⊢ Function.LeftInverse
    (fun x_1 ↦
      match x_1 with
      | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
    fun x_1 ↦
    match x_1 with
    | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
⊢ (commShiftIso ((F ⋙ G).obj ((shiftFunctor C₁' m).obj X₁')) n).hom.app X₂ ≫
      (shiftFunctor D n).map ((commShiftIso ((F ⋙ G).flip.obj X₂) m).hom.app X₁') =
    (commShiftIso ((F ⋙ G).flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app X₁' ≫
      (shiftFunctor D m).map ((commShiftIso ((F ⋙ G).obj X₁') n).hom.app X₂) ≫
        (shiftComm (((F ⋙ G).obj X₁').obj X₂) m n).inv ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj (((F ⋙ G).obj X₁').obj X₂)))

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₂' ⥤ C₂
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ NatTrans.CommShift ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).map f) M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
⊢ Function.RightInverse
    (fun x_1 ↦
      match x_1 with
      | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
    fun x_1 ↦
    match x_1 with
    | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (a, b + y) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y})
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y}
⊢ (a, b - y) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
⊢ (fun x ↦
        match x with
        | ⟨(a, b), h⟩ => ⟨(a, b - y), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => ⟨(a, b + y), ⋯⟩)
        x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y})
⊢ (fun x ↦
        match x with
        | ⟨(a, b), h⟩ => ⟨(a, b + y), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => ⟨(a, b - y), ⋯⟩)
        x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
⊢ ((shiftFunctor₂ C y ⋙ shiftFunctor₁ C x).obj K).HasTotal (up ℤ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
⊢ ((shiftFunctor₁ C x ⋙ shiftFunctor₂ C y).obj K).HasTotal (up ℤ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + x = n'
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + x, q) = n'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + x = n'
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n'
⊢ (up ℤ).π (up ℤ) (up ℤ) (p - x, q) = n

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₂' ⥤ C₂
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁ : C₁
X₂' : C₂'
m n : M
⊢ (commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj ((shiftFunctor C₁ m).obj X₁)) n).hom.app X₂' ≫
      (shiftFunctor D n).map ((commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).flip.obj X₂') m).hom.app X₁) =
    (commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).flip.obj ((shiftFunctor C₂' n).obj X₂')) m).hom.app X₁ ≫
      (shiftFunctor D m).map ((commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj X₁) n).hom.app X₂') ≫
        (shiftComm (((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj X₁).obj X₂') m n).inv ≫
          (↑(h.ε m n)).app
            ((shiftFunctor D n).obj ((shiftFunctor D m).obj (((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).obj X₁).obj X₂')))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h✝ : n + x = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
⊢ p + x - x = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + x = n'
⊢ ((((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) ≫
      K.totalDesc fun p q hpq ↦
        (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n ⋯) =
    𝟙 ((((shiftFunctor₁ C x).obj K).total (up ℤ)).X n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + x = n'
⊢ ((K.totalDesc fun p q hpq ↦
        (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) =
    𝟙 ((K.total (up ℤ)).X n')

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₁
⊢ CommShift ((𝟙 G₁).app x✝) M

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₂
⊢ CommShift (flipApp (𝟙 G₁) x✝) M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + 1, q) = n₁

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁹ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₁
⊢ CommShift ((τ ≫ τ').app x✝) M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + 1 + x, q) = n₁'

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} C₂'
inst✝⁹ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₂
⊢ CommShift (flipApp (τ ≫ τ') x✝) M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
⊢ ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

Tactic:
by

Goal state after: