awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α :=
    G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (a + b)) (G.obj (F.obj X)))
    (CategoryStruct.comp (Y :=
      G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
      (G.map
        (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X)))
      (CategoryStruct.comp (Y :=
        obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
        (NatTrans.app (Iso.hom (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
        (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (G.obj (F.obj X)))))
    (CategoryStruct.comp (Y :=
      G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
      (G.map
        (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (CategoryStruct.comp (Y :=
        obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
        (NatTrans.app (Iso.hom (commShiftIso G b)) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (map (shiftFunctor E b)
            (CategoryStruct.comp (Y := G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
              (G.map (NatTrans.app (Iso.hom (commShiftIso F a)) X))
              (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (G.obj (F.obj X)))))

Tactic:
simp only [map_comp, assoc, commShiftIso_hom_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_hom_naturality_assoc, CategoryTheory.Functor.map_comp
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (NatTrans.app (Iso.hom (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))) X)

Tactic:
have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add a b)) 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (NatTrans.app (Iso.hom (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))) X)
⊢ Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))

Tactic:
simp only [comp_obj, CommShift.isoAdd_hom_app,
    ← cancel_epi (F.map ((shiftFunctorAdd C a b).inv.app X)),
    ← F.map_comp_assoc, Iso.inv_hom_id_app, F.map_id, Category.id_comp] at eq

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, CategoryTheory.Functor.comp_obj, CategoryTheory.shiftFunctorAdd, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
simp :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' D a b (a + b) ⋯) ≪≫ shiftFunctorAdd' D b a (a + b) ⋯))
            (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm D a b)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
simp only [shiftFunctorComm_eq D a b _ rfl]

Premises used: CategoryTheory.shiftFunctorComm_eq, rfl
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
dsimp :
  Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        (NatTrans.app (Iso.inv (shiftFunctorAdd' D a b (a + b) ⋯)) (F.obj X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X)) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' D a b (a + b) ⋯) ≪≫ shiftFunctorAdd' D b a (a + b) ⋯))
            (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
dsimp
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
simp :
  Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd C a b) ≪≫ shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
⊢ Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        (NatTrans.app (Iso.inv (shiftFunctorAdd' D a b (a + b) ⋯)) (F.obj X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X)) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.assoc,
    ← reassoc_of% eq, shiftFunctorComm_eq C a b _ rfl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorComm_eq, rfl, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
dsimp :
  Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map
      (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
⊢ Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd C a b) ≪≫ shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
dsimp
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
rw :
  Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
⊢ Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map
      (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α :=
    F.obj (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)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
⊢ Eq (α :=
    F.obj (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)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b a (a + b) ⋯)) X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
        (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
        (NatTrans.app (Iso.hom (shiftFunctorAdd' D b a (a + b) ⋯)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
simp only [NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' (add_comm b a))) X,
    CommShift.isoAdd'_hom_app, Category.assoc, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
    Functor.map_id, Category.id_comp, comp_obj, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_add', CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, add_comm, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.CommShift.isoAdd'_hom_app, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Category.id_comp
-- 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 : C
a b : A
h : a + b = 0
dsimp :
  Eq (α :=
    F.obj (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)) ⟶ F.obj X)
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a b 0 h)) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶ F.obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C a b h)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a b h)) (F.obj X)))

Tactic:
dsimp [shiftFunctorCompIsoId]

Premises used: CategoryTheory.shiftFunctorCompIsoId
-- 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 : C
a b : A
h : a + b = 0
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F 0)) X)
    (NatTrans.app (Iso.hom (CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b))) X)

Tactic:
have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' h)) X