feat(category/has_shift): missing simp lemmas (#3365)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/graded_object.lean

@@ -125,13 +125,22 @@ def comap_equiv {β γ : Type w} (e : β ≃ γ) :
 
 end
 
-instance has_shift {β : Type} [add_comm_group β] (s : β) : has_shift (graded_object_with_shift s C) :=
+instance has_shift {β : Type*} [add_comm_group β] (s : β) : has_shift (graded_object_with_shift s C) :=
 { shift := comap_equiv C
   { to_fun := λ b, b-s,
     inv_fun := λ b, b+s,
     left_inv := λ x, (by simp),
     right_inv := λ x, (by simp), } }
 
+@[simp] lemma shift_functor_obj_apply {β : Type*} [add_comm_group β] (s : β) (X : β → C) (t : β) :
+  (shift (graded_object_with_shift s C)).functor.obj X t = X (t + s) :=
+rfl
+
+@[simp] lemma shift_functor_map_apply {β : Type*} [add_comm_group β] (s : β)
+  {X Y : graded_object_with_shift s C} (f : X ⟶ Y) (t : β) :
+  (shift (graded_object_with_shift s C)).functor.map f t = f (t + s) :=
+rfl
+
 instance has_zero_morphisms [has_zero_morphisms C] (β : Type w) :
   has_zero_morphisms.{(max w v)} (graded_object β C) :=
 { has_zero := λ X Y,