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
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C a ⋙ F₂).obj X ⟶ (F₁ ⋙ shiftFunctor D a).obj X)
      (app (Iso.hom (Functor.commShiftIso F₂ a) ≫ Functor.whiskerRight e.inv (shiftFunctor D a)) X)
      (app (Functor.whiskerLeft (shiftFunctor C a) e.inv ≫ Iso.hom (Functor.commShiftIso F₁ a)) X)
⊢ Eq (α := shiftFunctor C a ⋙ F₂ ⟶ F₁ ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso F₂ a) ≫ Functor.whiskerRight e.inv (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor C a) e.inv ≫ Iso.hom (Functor.commShiftIso F₁ a))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
w :
  Eq (α :=
    F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
⊢ Eq (α := (shiftFunctor C a ⋙ F₂).obj X ⟶ (F₁ ⋙ shiftFunctor D a).obj X)
    (app (Iso.hom (Functor.commShiftIso F₂ a) ≫ Functor.whiskerRight e.inv (shiftFunctor D a)) X)
    (app (Functor.whiskerLeft (shiftFunctor C a) e.inv ≫ Iso.hom (Functor.commShiftIso F₁ a)) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
⊢ CommShift e.symm.hom A

Tactic:
NatTrans.CommShift.of_iso_inv e A

Premises used: CategoryTheory.NatTrans.CommShift.of_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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : IsIso τ
inst_8 : CommShift τ A
⊢ CommShift (asIso τ).hom A

Tactic:
assumption
-- 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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : IsIso τ
inst_8 : CommShift τ A
⊢ CommShift (asIso τ).hom A

Tactic:
haveI : NatTrans.CommShift (asIso τ).hom A := by assumption
-- 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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : IsIso τ
inst_8 : CommShift τ A
this : CommShift (asIso τ).hom A
⊢ CommShift (asIso τ).inv A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift τ A
a : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C a ⋙ F₁ ⋙ G).obj X ⟶ ((F₂ ⋙ G) ⋙ shiftFunctor E a).obj X)
      (app
        (Iso.hom (Functor.commShiftIso (F₁ ⋙ G) a) ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a))
        X)
      (app
        (Functor.whiskerLeft (shiftFunctor C a) (Functor.whiskerRight τ G) ≫ Iso.hom (Functor.commShiftIso (F₂ ⋙ G) a))
        X)
⊢ Eq (α := shiftFunctor C a ⋙ F₁ ⋙ G ⟶ (F₂ ⋙ G) ⋙ shiftFunctor E a)
    (Iso.hom (Functor.commShiftIso (F₁ ⋙ G) a) ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a))
    (Functor.whiskerLeft (shiftFunctor C a) (Functor.whiskerRight τ G) ≫ Iso.hom (Functor.commShiftIso (F₂ ⋙ G) a))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift τ A
a : A
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ F₁ ⋙ G).obj X ⟶ ((F₂ ⋙ G) ⋙ shiftFunctor E a).obj X)
    (app
      (Iso.hom (Functor.commShiftIso (F₁ ⋙ G) a) ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a))
      X)
    (app (Functor.whiskerLeft (shiftFunctor C a) (Functor.whiskerRight τ G) ≫ Iso.hom (Functor.commShiftIso (F₂ ⋙ G) a))
      X)

Tactic:
simp only [Functor.whiskerRight_twice, comp_app, Functor.commShiftIso_comp_hom_app,
    Functor.associator_hom_app, Functor.whiskerRight_app, Functor.comp_map,
    Functor.associator_inv_app, comp_id, id_comp, assoc, ← Functor.commShiftIso_hom_naturality, ←
    G.map_comp_assoc, shift_app_comm, Functor.whiskerLeft_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.commShiftIso_hom_naturality, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.whiskerRight_twice, CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.Functor.comp_map, 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
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
w :
  ∀ (X : C),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ G).obj X ⟶ (G ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
      (NatTrans.app
        (Iso.hom
          (isoWhiskerLeft (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) e.symm ≪≫
            commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)))
        X)
      (NatTrans.app (Iso.hom (isoZero G A)) X)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ G ≅ G ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (isoWhiskerLeft (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) e.symm ≪≫
      commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0))
    (isoZero 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
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ G).obj X ⟶ (G ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
    (NatTrans.app
      (Iso.hom
        (isoWhiskerLeft (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) e.symm ≪≫
          commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)))
      X)
    (NatTrans.app (Iso.hom (isoZero G A)) X)

Tactic:
simp [F.commShiftIso_zero, ← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- 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
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C (a + b) ⋙ G).obj X ⟶ (G ⋙ shiftFunctor D (a + b)).obj X)
      (NatTrans.app
        (Iso.hom
          (isoWhiskerLeft (shiftFunctor C (a + b)) e.symm ≪≫
            commShiftIso F (a + b) ≪≫ isoWhiskerRight e (shiftFunctor D (a + b))))
        X)
      (NatTrans.app
        (Iso.hom
          (isoAdd (isoWhiskerLeft (shiftFunctor C a) e.symm ≪≫ commShiftIso F a ≪≫ isoWhiskerRight e (shiftFunctor D a))
            (isoWhiskerLeft (shiftFunctor C b) e.symm ≪≫ commShiftIso F b ≪≫ isoWhiskerRight e (shiftFunctor D b))))
        X)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ G ≅ G ⋙ shiftFunctor D (a + b))
    (isoWhiskerLeft (shiftFunctor C (a + b)) e.symm ≪≫
      commShiftIso F (a + b) ≪≫ isoWhiskerRight e (shiftFunctor D (a + b)))
    (isoAdd (isoWhiskerLeft (shiftFunctor C a) e.symm ≪≫ commShiftIso F a ≪≫ isoWhiskerRight e (shiftFunctor D a))
      (isoWhiskerLeft (shiftFunctor C b) e.symm ≪≫ commShiftIso F b ≪≫ isoWhiskerRight e (shiftFunctor D b)))

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
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
X : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
    (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) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd 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) (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          map (shiftFunctor D b) (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            CategoryStruct.comp (Y :=
              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)))
              (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
              (map (shiftFunctor D b) (map (shiftFunctor D a) (e.hom.app X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X))))
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ G).obj X ⟶ (G ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app
      (Iso.hom
        (isoWhiskerLeft (shiftFunctor C (a + b)) e.symm ≪≫
          commShiftIso F (a + b) ≪≫ isoWhiskerRight e (shiftFunctor D (a + b))))
      X)
    (NatTrans.app
      (Iso.hom
        (isoAdd (isoWhiskerLeft (shiftFunctor C a) e.symm ≪≫ commShiftIso F a ≪≫ isoWhiskerRight e (shiftFunctor D a))
          (isoWhiskerLeft (shiftFunctor C b) e.symm ≪≫ commShiftIso F b ≪≫ isoWhiskerRight e (shiftFunctor D b))))
      X)

Tactic:
simp only [comp_obj, F.commShiftIso_add, Iso.trans_hom, isoWhiskerLeft_hom,
      Iso.symm_hom, isoWhiskerRight_hom, NatTrans.comp_app, whiskerLeft_app,
      isoAdd_hom_app, whiskerRight_app, assoc, map_comp, NatTrans.naturality_assoc,
      NatIso.cancel_natIso_inv_left]

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.commShiftIso_add, CategoryTheory.Iso.symm_hom, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.isoWhiskerRight_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.isoWhiskerLeft_hom, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.NatIso.cancel_natIso_inv_left
-- 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
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
X : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
    (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) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd 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 ≫ map (shiftFunctor D a) (e.hom.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
    (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) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd 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) (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          map (shiftFunctor D b) (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            CategoryStruct.comp (Y :=
              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)))
              (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
              (map (shiftFunctor D b) (map (shiftFunctor D a) (e.hom.app X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X))))

Tactic:
simp only [← Functor.map_comp_assoc, e.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc
-- 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
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
X : C
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
    (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) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd 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 ≫ map (shiftFunctor D a) (e.hom.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X)))

Tactic:
simp only [← NatTrans.naturality, comp_obj, comp_map, map_comp, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- 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 G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
this : G.CommShift A := ofIso e A
a : A
w :
  ∀ (x : C),
    Eq (α := (shiftFunctor C a ⋙ F).obj x ⟶ (G ⋙ shiftFunctor D a).obj x)
      (NatTrans.app (Iso.hom (commShiftIso F a) ≫ whiskerRight e.hom (shiftFunctor D a)) x)
      (NatTrans.app (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso G a)) x)
⊢ Eq (α := shiftFunctor C a ⋙ F ⟶ G ⋙ shiftFunctor D a)
    (Iso.hom (commShiftIso F a) ≫ whiskerRight e.hom (shiftFunctor D a))
    (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso G a))

Tactic:
ext
-- 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 G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
this : G.CommShift A := ofIso e A
a : A
x : C
⊢ Eq (α := (shiftFunctor C a ⋙ F).obj x ⟶ (G ⋙ shiftFunctor D a).obj x)
    (NatTrans.app (Iso.hom (commShiftIso F a) ≫ whiskerRight e.hom (shiftFunctor D a)) x)
    (NatTrans.app (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso G a)) x)

Tactic:
simp [ofIso_commShiftIso_hom_app]

Premises used: CategoryTheory.Functor.CommShift.ofIso_commShiftIso_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 G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
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
this : G.CommShift A := ofIso e A
⊢ NatTrans.CommShift e.hom A

Tactic:
exact ⟨fun a => by ext; simp [ofIso_commShiftIso_hom_app]⟩
-- 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
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
w :
  ∀ (X : C),
    Eq (α := (s 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X) (NatTrans.app (Iso.hom (i 0)) X)
      (NatTrans.app (Iso.hom (isoZero F A)) X)
⊢ 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) (i 0)
    (isoZero F 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
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
X : C
⊢ Eq (α := (s 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X) (NatTrans.app (Iso.hom (i 0)) X)
    (NatTrans.app (Iso.hom (isoZero F A)) X)

Tactic:
simp [ShiftMkCore.shiftFunctorZero_eq]

Premises used: CategoryTheory.ShiftMkCore.shiftFunctorZero_eq
-- 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
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
a b : A
w :
  ∀ (X : C),
    Eq (α := (s (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X) (NatTrans.app (Iso.hom (i (a + b))) X)
      (NatTrans.app (Iso.hom (isoAdd (i a) (i b))) X)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (i (a + b)) (isoAdd (i a) (i b))

Tactic:
ext X