mathlib-initiative/mathlib-tactics huggingface dataset:
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
X : C
⊢ ((lift r F hF).map (𝟙 ((shiftFunctor C a ⋙ functor r).obj X)) ≫ (Functor.commShiftIso F a).hom.app X) ≫
      (shiftFunctor D a).map (𝟙 (F.obj X)) =
    𝟙 (F.obj ((shiftFunctor C a).obj X)) ≫ (Functor.commShiftIso F a).hom.app X

Tactic:
]

Goal state after:
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
X : C
⊢ ((lift r F hF).map (𝟙 ((shiftFunctor C a ⋙ functor r).obj X)) ≫ (Functor.commShiftIso F a).hom.app X) ≫
      (shiftFunctor D a).map (𝟙 (F.obj X)) =
    𝟙 (F.obj ((shiftFunctor C a).obj X)) ≫ (Functor.commShiftIso F a).hom.app X
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 + (b + a) = n + (b + a)

Tactic:
]

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 : ℤ
⊢ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom

Tactic:
]

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

Tactic:
]

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 p q : ℤ
hpq : p = q
⊢ q + n = q + n

Tactic:
]

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' C a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ (XIsoOfEq x✝ ⋯).hom = (XIsoOfEq x✝ ⋯).hom

Tactic:
]

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 + (a + b) = p + (a + b)

Tactic:
]

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 p : ℤ
⊢ (((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).symm ≪≫
                CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app
          K).f
      p =
    (XIsoOfEq K ⋯).hom

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).symm ≪≫
                CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app
          K).f
      p =
    (XIsoOfEq K ⋯).hom
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
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X) ≫
          (((s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X)) ≫
                (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X))) ≫
              (s m₃).map ((s m₂).map ((i m₁).inv.app X))) ≫
            (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.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
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X) ≫
          (((s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X)) ≫
                (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X))) ≫
              (s m₃).map ((s m₂).map ((i m₁).inv.app X))) ≫
            (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))
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 : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
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 ℤ
⊢ n + i = n + i

Tactic:
]

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✝
i✝ : ℤ
⊢ F.map (x✝.f (i✝ + n)) = F.map (x✝.f (i✝ + n))

Tactic:
]

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
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ ((F.mapCochainComplexShiftIso 0).hom.app x✝).f i✝ =
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map
            ((shiftFunctorZero (HomologicalComplex C (ComplexShape.up ℤ)) ℤ).hom.app x✝) ≫
          (shiftFunctorZero (HomologicalComplex D (ComplexShape.up ℤ)) ℤ).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
      i✝

Tactic:
]

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
F : C ⥤ D
inst✝ : F.Additive
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ ((F.mapCochainComplexShiftIso 0).hom.app x✝).f i✝ =
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map
            ((shiftFunctorZero (HomologicalComplex C (ComplexShape.up ℤ)) ℤ).hom.app x✝) ≫
          (shiftFunctorZero (HomologicalComplex D (ComplexShape.up ℤ)) ℤ).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
      i✝
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 : ℤ
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ ((F.mapCochainComplexShiftIso (a + b)).hom.app x✝).f i✝ =
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map
            ((shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) a b).hom.app x✝) ≫
          (F.mapCochainComplexShiftIso b).hom.app ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) a).obj x✝) ≫
            (shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) b).map
                ((F.mapCochainComplexShiftIso a).hom.app x✝) ≫
              (shiftFunctorAdd (HomologicalComplex D (ComplexShape.up ℤ)) a b).inv.app
                ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
      i✝

Tactic:
]

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
F : C ⥤ D
inst✝ : F.Additive
a b : ℤ
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ ((F.mapCochainComplexShiftIso (a + b)).hom.app x✝).f i✝ =
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map
            ((shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) a b).hom.app x✝) ≫
          (F.mapCochainComplexShiftIso b).hom.app ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) a).obj x✝) ≫
            (shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) b).map
                ((F.mapCochainComplexShiftIso a).hom.app x✝) ≫
              (shiftFunctorAdd (HomologicalComplex D (ComplexShape.up ℤ)) a b).inv.app
                ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
      i✝
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 : ℤ
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ 𝟙 (F.obj (x✝.X (i✝ + (a + b)))) =
    F.map (((shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) a b).hom.app x✝).f i✝) ≫
      ((shiftFunctorAdd (HomologicalComplex D (ComplexShape.up ℤ)) a b).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
        i✝

Tactic:
]

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
F : C ⥤ D
inst✝ : F.Additive
a b : ℤ
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ 𝟙 (F.obj (x✝.X (i✝ + (a + b)))) =
    F.map (((shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) a b).hom.app x✝).f i✝) ≫
      ((shiftFunctorAdd (HomologicalComplex D (ComplexShape.up ℤ)) a b).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
        i✝
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
⊢ 0 = 0

pp: case a
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
⊢ ¬(ComplexShape.up ℤ).Rel (j + n) (i + n)

Tactic:
]

Goal state after:
case a
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
⊢ ¬(ComplexShape.up ℤ).Rel (j + n) (i + n)
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 =
    ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K).d i (i + 1) ≫
          (n.negOnePow • h.hom (i + 1 + { as := n }.as) (i + { as := n }.as)) +
        (n.negOnePow • h.hom (i + { as := n }.as) (i - 1 + { as := n }.as)) ≫
          ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L).d (i - 1) i +
      ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₂).f i

Tactic:
]

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 L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₁).f i =
    ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K).d i (i + 1) ≫
          (n.negOnePow • h.hom (i + 1 + { as := n }.as) (i + { as := n }.as)) +
        (n.negOnePow • h.hom (i + { as := n }.as) (i - 1 + { as := n }.as)) ≫
          ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L).d (i - 1) i +
      ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₂).f i
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 + (n' + a) = p + (n' + a)

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
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
⊢ q = q

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
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ p + n = p + n

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
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ p' + a = p' + a

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
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : HasShift C B
inst✝ : HasShift D B
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ a + b + c = abc

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : AddCommMonoid B
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : HasShift C B
inst✝ : HasShift D B
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ a + b + c = abc
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
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (shiftFunctor C m₃ ⋙ F).map ((shiftFunctorAdd C m₁ m₂).hom.app X) ≫
          (i m₃).inv.app ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X) ≫
            (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))

Tactic:
reassoc_of% eq,

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
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map (eqToHom ⋯) ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)) ≫
            (i m₃).inv.app ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X) ≫
              (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.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
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map (eqToHom ⋯) ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)) ≫
            (i m₃).inv.app ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X) ≫
              (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (eqToHom ⋯ ≫ (i (m₁ + m₂ + m₃)).hom.app X ≫ eqToHom ⋯) ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.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
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map (eqToHom ⋯) ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)) ≫
            (i m₃).inv.app ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X) ≫
              (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (eqToHom ⋯ ≫ (i (m₁ + m₂ + m₃)).hom.app X ≫ eqToHom ⋯) ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.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 = 𝟭 D ⋙ s n

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 = 𝟭 D ⋙ s n
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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ p + (n + a) = p + (n + a)

Tactic:
]

Goal state after: