awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} 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
⊢ Eq (α :=
    (shiftFunctor C c ⋙ F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X) ⟶
      (F ⋙ shiftFunctor D c).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
    ((shiftFunctor C c ⋙ F).map (Iso.hom (Iso.app (shiftFunctorAdd' C a b ab hab) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ≫
        (F ⋙ shiftFunctor D c).map (Iso.inv (Iso.app (shiftFunctorAdd' C a b ab hab) X)))
    (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))

Tactic:
have := NatTrans.naturality_2 ec.hom ((shiftFunctorAdd' C a b ab hab).app X)
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} 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
this :
  Eq (α :=
    (shiftFunctor C c ⋙ F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X) ⟶
      (F ⋙ shiftFunctor D c).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
    ((shiftFunctor C c ⋙ F).map (Iso.hom (Iso.app (shiftFunctorAdd' C a b ab hab) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ≫
        (F ⋙ shiftFunctor D c).map (Iso.inv (Iso.app (shiftFunctorAdd' C a b ab hab) X)))
    (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C abc) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D abc) (F.obj X))
    (NatTrans.app (Iso.hom (isoAdd' ⋯ (isoAdd' hab ea eb) ec)) X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ ea (isoAdd' hbc eb ec))) X)
⊢ Eq (α := (shiftFunctor C abc ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D abc).obj X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ (isoAdd' hab ea eb) ec)) X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ ea (isoAdd' hbc eb ec))) X)

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} 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
this :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D c) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)))
    (F.map (map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D c) (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b ab hab)) X)))
    (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C abc) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D abc) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C ab c abc ⋯)) X) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X) ≫
        map (shiftFunctor D c)
            (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X) ≫
              eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                map (shiftFunctor D b) (ea.hom.app X) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd' D a b ab hab)) (F.obj X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D ab c abc ⋯)) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc ⋯)) X) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          map (shiftFunctor D c) (eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b c bc hbc))
                (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
              map (shiftFunctor D bc) (ea.hom.app X) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' D a bc abc ⋯)) (F.obj X))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C abc) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D abc) (F.obj X))
    (NatTrans.app (Iso.hom (isoAdd' ⋯ (isoAdd' hab ea eb) ec)) X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ ea (isoAdd' hbc eb ec))) X)

Tactic:
simp only [isoAdd'_hom_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.isoAdd'_hom_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} 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
this :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D c) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)))
    (F.map (map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D c) (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b ab hab)) X)))
    (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
⊢ F.map
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc ⋯)) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D c)
            (F.map
                (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b ab hab)) X ≫
                  NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X) ≫
              eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                map (shiftFunctor D b) (ea.hom.app X) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd' D a b ab hab)) (F.obj X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D ab c abc ⋯)) (F.obj X) =
    F.map
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc ⋯)) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D c) (eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          map (shiftFunctor D b ⋙ shiftFunctor D c) (ea.hom.app X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b c bc hbc))
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' D a bc abc ⋯)) (F.obj X)

Tactic:
simp [shiftFunctorAdd'_assoc_inv_app a b c ab bc abc hab hbc h]

Premises used: CategoryTheory.shiftFunctorAdd'_assoc_inv_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X Y : C
f : X ⟶ Y
a : A
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj Y))
    (F.map (map (shiftFunctor C a) f) ≫ NatTrans.app (Iso.hom (commShiftIso F a)) Y)
    (NatTrans.app (Iso.hom (commShiftIso F a)) X ≫ map (shiftFunctor D a) (F.map f))

Tactic:
(F.commShiftIso a).hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
X Y : C
f : X ⟶ Y
a : A
⊢ Eq (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X) ⟶ F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y))
    (map (shiftFunctor D a) (F.map f) ≫ NatTrans.app (Iso.inv (commShiftIso F a)) Y)
    (NatTrans.app (Iso.inv (commShiftIso F a)) X ≫ F.map (map (shiftFunctor C a) f))

Tactic:
(F.commShiftIso a).inv.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
a : A
h : a = 0
subst :
  Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (commShiftIso F 0) (CommShift.isoZero' F A 0 ⋯)
⊢ Eq (α := shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a) (commShiftIso F a) (CommShift.isoZero' F A a h)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
rw :
  Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (commShiftIso F 0) (CommShift.isoZero F A)
rw₁ rw₂ :
  Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (CommShift.isoZero F A) (CommShift.isoZero F A)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (commShiftIso F 0) (CommShift.isoZero' F A 0 ⋯)

Tactic:
rw [CommShift.isoZero'_eq_isoZero, commShiftIso_zero]

Premises used: CategoryTheory.Functor.CommShift.isoZero'_eq_isoZero, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
a b c : A
h : a + b = c
subst :
  Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (commShiftIso F (a + b))
    (CommShift.isoAdd' ⋯ (commShiftIso F a) (commShiftIso F b))
⊢ Eq (α := shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c) (commShiftIso F c)
    (CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (commShiftIso F (a + b))
    (CommShift.isoAdd' ⋯ (commShiftIso F a) (commShiftIso F b))

Tactic:
simp only [commShiftIso_add, CommShift.isoAdd]

Premises used: CategoryTheory.Functor.CommShift.isoAdd, CategoryTheory.Functor.CommShift.commShiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
w :
  ∀ (X : C),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ⋙ G).obj X ⟶
        ((F ⋙ G) ⋙ shiftFunctor.{v_3, u_3, u_4} E (A := A) 0).obj X)
      (NatTrans.app
        (Iso.hom
          (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) F G) ≪≫
            isoWhiskerRight (commShiftIso F 0) G ≪≫
              F.associator (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) G ≪≫
                F.isoWhiskerLeft (commShiftIso G 0) ≪≫
                  (F.associator G (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)).symm))
        X)
      (NatTrans.app (Iso.hom (isoZero (F ⋙ G) A)) X)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ⋙ G ≅ (F ⋙ G) ⋙ shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)
    (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) F G) ≪≫
      isoWhiskerRight (commShiftIso F 0) G ≪≫
        F.associator (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) G ≪≫
          F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)).symm)
    (isoZero (F ⋙ G) A)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
X : C
w :
  𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))) ≫
      G.map (NatTrans.app (Iso.hom (commShiftIso F 0)) X) ≫
        𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))) ≫
          NatTrans.app (Iso.hom (commShiftIso G 0)) (F.obj X) ≫
            𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0) (G.obj (F.obj X))) =
    NatTrans.app (Iso.hom (isoZero (F ⋙ G) A)) X
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ⋙ G).obj X ⟶
      ((F ⋙ G) ⋙ shiftFunctor.{v_3, u_3, u_4} E (A := A) 0).obj X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) F G) ≪≫
          isoWhiskerRight (commShiftIso F 0) G ≪≫
            F.associator (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) G ≪≫
              F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)).symm))
      X)
    (NatTrans.app (Iso.hom (isoZero (F ⋙ G) A)) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
X : C
⊢ 𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))) ≫
      G.map (NatTrans.app (Iso.hom (commShiftIso F 0)) X) ≫
        𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))) ≫
          NatTrans.app (Iso.hom (commShiftIso G 0)) (F.obj X) ≫
            𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0) (G.obj (F.obj X))) =
    NatTrans.app (Iso.hom (isoZero (F ⋙ G) A)) X

Tactic:
simp only [id_comp, comp_id, commShiftIso_zero, isoZero_hom_app, ← Functor.map_comp_assoc,
      assoc, Iso.inv_hom_id_app, id_obj, comp_map, comp_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.CommShift.commShiftIso_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
a b : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C (a + b) ⋙ F ⋙ G).obj X ⟶ ((F ⋙ G) ⋙ shiftFunctor E (a + b)).obj X)
      (NatTrans.app
        (Iso.hom
          (Iso.symm (associator (shiftFunctor C (a + b)) F G) ≪≫
            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))
        X)
      (NatTrans.app
        (Iso.hom
          (isoAdd
            (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
              isoWhiskerRight (commShiftIso F a) G ≪≫
                F.associator (shiftFunctor D a) G ≪≫
                  F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
            (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
              isoWhiskerRight (commShiftIso F b) G ≪≫
                F.associator (shiftFunctor D b) G ≪≫
                  F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)))
        X)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ⋙ G ≅ (F ⋙ G) ⋙ shiftFunctor E (a + b))
    (Iso.symm (associator (shiftFunctor C (a + b)) F G) ≪≫
      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
      (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
        isoWhiskerRight (commShiftIso F a) G ≪≫
          F.associator (shiftFunctor D a) G ≪≫
            F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
      (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
        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
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
a b : A
X : C
w :
  𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X))) ≫
      G.map (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X) ≫
        𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))) ≫
          NatTrans.app (Iso.hom (commShiftIso G (a + b))) (F.obj X) ≫
            𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (a + b)) (G.obj (F.obj X))) =
    NatTrans.app
      (Iso.hom
        (isoAdd
          (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
            isoWhiskerRight (commShiftIso F a) G ≪≫
              F.associator (shiftFunctor D a) G ≪≫
                F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
          (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
            isoWhiskerRight (commShiftIso F b) G ≪≫
              F.associator (shiftFunctor D b) G ≪≫
                F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)))
      X
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F ⋙ G).obj X ⟶ ((F ⋙ G) ⋙ shiftFunctor E (a + b)).obj X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor C (a + b)) F G) ≪≫
          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))
      X)
    (NatTrans.app
      (Iso.hom
        (isoAdd
          (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
            isoWhiskerRight (commShiftIso F a) G ≪≫
              F.associator (shiftFunctor D a) G ≪≫
                F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
          (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
            isoWhiskerRight (commShiftIso F b) G ≪≫
              F.associator (shiftFunctor D b) G ≪≫
                F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)))
      X)

Tactic:
dsimp