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 b : A
⊢ (functor r).whiskerLeft (LiftCommShift.iso F r hF (a + b)).hom =
    (functor r).whiskerLeft (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)).hom

Tactic:
ext X

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 b : A
X : C
⊢ ((functor r).whiskerLeft (LiftCommShift.iso F r hF (a + b)).hom).app X =
    ((functor r).whiskerLeft
          (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)).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
n : ℤ
K : CochainComplex C ℤ
i✝ j✝ k✝ : ℤ
a✝¹ : (ComplexShape.up ℤ).Rel i✝ j✝
a✝ : (ComplexShape.up ℤ).Rel j✝ k✝
⊢ (n.negOnePow • K.d (i✝ + n) (j✝ + n)) ≫ (n.negOnePow • K.d (j✝ + n) (k✝ + n)) = 0

Tactic:
simp only [Linear.comp_units_smul, Linear.units_smul_comp, d_comp_d, smul_zero]

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:
ext X

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
⊢ ((Functor.commShiftIso (functor r ⋙ lift r F hF) a).hom ≫
          Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a)).app
      X =
    ((shiftFunctor C a).whiskerLeft (lift.isLift r F hF).hom ≫ (Functor.commShiftIso F a).hom).app X
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 ((Functor.commShiftIso (functor r) a).hom.app X) ≫
        (lift r F hF).map ((Functor.commShiftIso (functor r) a).inv.app 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:
← Functor.map_comp_assoc,

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 ((Functor.commShiftIso (functor r) a).hom.app X ≫ (Functor.commShiftIso (functor r) a).inv.app 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
n : ℤ
this : (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive

Tactic:
apply Functor.additive_of_full_essSurj_comp (quotient _ _)

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
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
⊢ isoAdd' ⋯ e (isoZero F A) = e

Tactic:
ext 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 : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
⊢ (isoAdd' ⋯ e (isoZero F A)).hom.app X = e.hom.app 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
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
⊢ isoAdd' ⋯ (isoZero F A) e = e

Tactic:
ext 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 : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
⊢ (isoAdd' ⋯ (isoZero F A) e).hom.app X = e.hom.app 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
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
⊢ isoAdd' ⋯ (isoAdd' hab ea eb) ec = isoAdd' ⋯ ea (isoAdd' hbc eb ec)

Tactic:
ext 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 : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
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
X : C
⊢ (isoAdd' ⋯ (isoAdd' hab ea eb) ec).hom.app X = (isoAdd' ⋯ ea (isoAdd' hbc eb ec)).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
⊢ ((whiskeringLeft C D D).obj F).map (Induced.add F s i 0 n).hom =
    ((whiskeringLeft C D D).obj F).map (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))

Tactic:
ext X

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
⊢ (((whiskeringLeft C D D).obj F).map (Induced.add F s i 0 n).hom).app X =
    (((whiskeringLeft C D D).obj F).map (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))).app 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ p' + n = q'

Tactic:
by rw [hp', hq', ← hpq, add_assoc, add_comm a, add_assoc]

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
⊢ ((whiskeringLeft C D D).obj F).map (Induced.add F s i n 0).hom =
    ((whiskeringLeft C D D).obj F).map (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)

Tactic:
ext X

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
⊢ (((whiskeringLeft C D D).obj F).map (Induced.add F s i n 0).hom).app X =
    (((whiskeringLeft C D D).obj F).map (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)).app X
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
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
⊢ ((shiftFunctor C 0).associator F G).symm ≪≫
      isoWhiskerRight (commShiftIso F 0) G ≪≫
        F.associator (shiftFunctor D 0) G ≪≫
          F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor E 0)).symm =
    isoZero (F ⋙ G) A

Tactic:
ext X

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
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
X : C
⊢ (((shiftFunctor C 0).associator F G).symm ≪≫
            isoWhiskerRight (commShiftIso F 0) G ≪≫
              F.associator (shiftFunctor D 0) G ≪≫
                F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor E 0)).symm).hom.app
      X =
    (isoZero (F ⋙ G) A).hom.app X
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
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a b : A
⊢ ((shiftFunctor C (a + b)).associator F G).symm ≪≫
      isoWhiskerRight (commShiftIso F (a + b)) G ≪≫
        F.associator (shiftFunctor D (a + b)) G ≪≫
          F.isoWhiskerLeft (commShiftIso G (a + b)) ≪≫ (F.associator G (shiftFunctor E (a + b))).symm =
    isoAdd
      (((shiftFunctor C a).associator F G).symm ≪≫
        isoWhiskerRight (commShiftIso F a) G ≪≫
          F.associator (shiftFunctor D a) G ≪≫
            F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
      (((shiftFunctor C b).associator F G).symm ≪≫
        isoWhiskerRight (commShiftIso F b) G ≪≫
          F.associator (shiftFunctor D b) G ≪≫
            F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)

Tactic:
ext X

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
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a b : A
X : C
⊢ (((shiftFunctor C (a + b)).associator F G).symm ≪≫
            isoWhiskerRight (commShiftIso F (a + b)) G ≪≫
              F.associator (shiftFunctor D (a + b)) G ≪≫
                F.isoWhiskerLeft (commShiftIso G (a + b)) ≪≫ (F.associator G (shiftFunctor E (a + b))).symm).hom.app
      X =
    (isoAdd
            (((shiftFunctor C a).associator F G).symm ≪≫
              isoWhiskerRight (commShiftIso F a) G ≪≫
                F.associator (shiftFunctor D a) G ≪≫
                  F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
            (((shiftFunctor C b).associator F G).symm ≪≫
              isoWhiskerRight (commShiftIso F b) G ≪≫
                F.associator (shiftFunctor D b) G ≪≫
                  F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)).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
this : HasShift D A := HasShift.induced F A s i
⊢ (i 0).symm = isoZero F A

Tactic:
ext X

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
X : C
⊢ (i 0).symm.hom.app X = (isoZero F A).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
this : HasShift D A := HasShift.induced F A s i
a b : A
⊢ (i (a + b)).symm = isoAdd (i a).symm (i b).symm

Tactic:
ext X

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)).symm.hom.app X = (isoAdd (i a).symm (i b).symm).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
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 ((i a).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:
← Functor.map_comp_assoc,

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 ((i a).inv.app X ≫ (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
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.map ((shiftFunctorCompIsoId C a b h).inv.app 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:
rw [← cancel_epi (F.map ((shiftFunctorCompIsoId C a b h).hom.app X)), ← F.map_comp,
    Iso.hom_inv_id_app, F.map_id, map_shiftFunctorCompIsoId_hom_app]

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
⊢ (Functor.commShiftIso F₁ 0).hom ≫ Functor.whiskerRight τ (shiftFunctor D 0) =
    (shiftFunctor C 0).whiskerLeft τ ≫ (Functor.commShiftIso F₂ 0).hom

Tactic:
ext 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
X : C
⊢ ((Functor.commShiftIso F₁ 0).hom ≫ Functor.whiskerRight τ (shiftFunctor D 0)).app X =
    ((shiftFunctor C 0).whiskerLeft τ ≫ (Functor.commShiftIso F₂ 0).hom).app 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 b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
⊢ (Functor.commShiftIso F₁ (a + b)).hom ≫ Functor.whiskerRight τ (shiftFunctor D (a + b)) =
    (shiftFunctor C (a + b)).whiskerLeft τ ≫ (Functor.commShiftIso F₂ (a + b)).hom

Tactic:
ext 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
⊢ ((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.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
⊢ (Functor.commShiftIso F₂ a).hom ≫ Functor.whiskerRight e.inv (shiftFunctor D a) =
    (shiftFunctor C a).whiskerLeft e.inv ≫ (Functor.commShiftIso F₁ a).hom

Tactic:
ext X

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

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} E
inst✝¹² : Category.{v_4, u_4} J
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : D ⥤ E
τ'' : G ⟶ G'
H : E ⥤ J
A : Type u_5
inst✝¹¹ : AddMonoid A
inst✝¹⁰ : HasShift C A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
inst✝⁷ : HasShift J A
inst✝⁶ : F₁.CommShift A
inst✝⁵ : F₂.CommShift A
inst✝⁴ : F₃.CommShift A
inst✝³ : G.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : H.CommShift A
inst✝ : CommShift τ A
a : A
X : C
⊢ ((Functor.commShiftIso (F₁ ⋙ G) a).hom ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a)).app X =
    ((shiftFunctor C a).whiskerLeft (Functor.whiskerRight τ G) ≫ (Functor.commShiftIso (F₂ ⋙ G) a).hom).app X
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
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ (shiftFunctor C 0).isoWhiskerLeft e.symm ≪≫ commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor D 0) = isoZero G A

Tactic:
ext X

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
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
⊢ ((shiftFunctor C 0).isoWhiskerLeft e.symm ≪≫ commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor D 0)).hom.app X =
    (isoZero G A).hom.app X