refactor(category_theory/shift): improve automation (#18670)

src/category_theory/differential_object.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import data.int.basic
-import category_theory.shift
+import category_theory.shift.basic
 import category_theory.concrete_category.basic
 
 /-!
@@ -220,52 +220,67 @@ def shift_functor (n : ℤ) : differential_object C ⥤ differential_object C :=
         ←functor.map_comp_assoc, X.d_squared, functor.map_zero, zero_comp] },
   map := λ X Y f,
   { f := f.f⟦n⟧',
-    comm' := by { dsimp, rw [category.assoc, shift_comm_hom_comp, ← functor.map_comp_assoc,
-      f.comm, functor.map_comp_assoc], }, },
+    comm' := begin
+      dsimp,
+      erw [category.assoc, shift_comm_hom_comp, ← functor.map_comp_assoc, f.comm,
+        functor.map_comp_assoc],
+      refl,
+    end, },
   map_id' := by { intros X, ext1, dsimp, rw functor.map_id },
   map_comp' := by { intros X Y Z f g, ext1, dsimp, rw functor.map_comp } }
 
-local attribute [simp] eq_to_hom_map
-local attribute [reducible] discrete.add_monoidal shift_comm
-
 /-- The shift functor on `differential_object C` is additive. -/
 @[simps] def shift_functor_add (m n : ℤ) :
   shift_functor C (m + n) ≅ shift_functor C m ⋙ shift_functor C n :=
 begin
   refine nat_iso.of_components (λ X, mk_iso (shift_add X.X _ _) _) _,
   { dsimp,
-    -- This is just `simp, simp [eq_to_hom_map]`.
-    simp_rw [category.assoc, obj_μ_inv_app, μ_inv_hom_app_assoc, functor.map_comp, obj_μ_app,
-      category.assoc, μ_naturality_assoc, μ_inv_hom_app_assoc, obj_μ_inv_app, category.assoc,
-      μ_naturalityₗ_assoc, μ_inv_hom_app_assoc, μ_inv_naturalityᵣ_assoc],
-    simp only [eq_to_hom_map, eq_to_hom_app, eq_to_iso.hom, eq_to_hom_trans_assoc,
-      eq_to_iso.inv], },
+    rw [← cancel_epi ((shift_functor_add C m n).inv.app X.X)],
+    simp only [category.assoc, iso.inv_hom_id_app_assoc],
+    erw [← nat_trans.naturality_assoc],
+    dsimp,
+    simp only [functor.map_comp, category.assoc,
+      shift_functor_comm_hom_app_comp_shift_shift_functor_add_hom_app 1 m n X.X,
+      iso.inv_hom_id_app_assoc], },
   { intros X Y f, ext, dsimp, exact nat_trans.naturality _ _ }
 end
 
-local attribute [reducible] endofunctor_monoidal_category
-
 section
-local attribute [instance] endofunctor_monoidal_category
 
 /-- The shift by zero is naturally isomorphic to the identity. -/
 @[simps]
-def shift_ε : 𝟭 (differential_object C) ≅ shift_functor C 0 :=
+def shift_zero : shift_functor C 0 ≅ 𝟭 (differential_object C) :=
 begin
-  refine nat_iso.of_components (λ X, mk_iso ((shift_monoidal_functor C ℤ).ε_iso.app X.X) _) _,
-  { dsimp, simp, dsimp, simp },
-  { introv, ext, dsimp, simp }
+  refine nat_iso.of_components (λ X, mk_iso ((shift_functor_zero C ℤ).app X.X) _) _,
+  { erw [← nat_trans.naturality],
+    dsimp,
+    simp only [shift_functor_zero_hom_app_shift, category.assoc], },
+  { tidy, },
 end
 
 end
 
-local attribute [simp] eq_to_hom_map
-
 instance : has_shift (differential_object C) ℤ :=
 has_shift_mk _ _
 { F := shift_functor C,
-  ε := shift_ε C,
-  μ := λ m n, (shift_functor_add C m n).symm }
+  zero := shift_zero C,
+  add := shift_functor_add C,
+  assoc_hom_app := λ m₁ m₂ m₃ X, begin
+    ext1,
+    convert shift_functor_add_assoc_hom_app m₁ m₂ m₃ X.X,
+    dsimp [shift_functor_add'],
+    simpa,
+  end,
+  zero_add_hom_app := λ n X, begin
+    ext1,
+    convert shift_functor_add_zero_add_hom_app n X.X,
+    simpa,
+  end,
+  add_zero_hom_app := λ n X, begin
+    ext1,
+    convert shift_functor_add_add_zero_hom_app n X.X,
+    simpa,
+  end, }
 
 end differential_object
 

src/category_theory/graded_object.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import algebra.group_power.lemmas
 import category_theory.pi.basic
-import category_theory.shift
+import category_theory.shift.basic
 import category_theory.concrete_category.basic
 
 /-!
@@ -106,11 +106,12 @@ instance has_shift {β : Type*} [add_comm_group β] (s : β) :
   has_shift (graded_object_with_shift s C) ℤ :=
 has_shift_mk _ _
 { F := λ n, comap (λ _, C) $ λ (b : β), b + n • s,
-  ε := (comap_id β (λ _, C)).symm ≪≫ (comap_eq C (by { ext, simp })),
-  μ := λ m n, comap_comp _ _ _ ≪≫ comap_eq C (by { ext, simp [add_zsmul, add_comm] }),
-  left_unitality := by { introv, ext, dsimp, simpa },
-  right_unitality := by { introv, ext, dsimp, simpa },
-  associativity := by { introv, ext, dsimp, simp } }
+  zero := comap_eq C (by { ext, simp }) ≪≫ comap_id β (λ _, C),
+  add := λ m n,  comap_eq C (by { ext, simp [add_zsmul, add_comm], }) ≪≫
+    (comap_comp _ _ _).symm,
+  assoc_hom_app := λ m₁ m₂ m₃ X, by { ext, dsimp, simp, },
+  zero_add_hom_app := λ n X, by { ext, dsimp, simpa, },
+  add_zero_hom_app := λ n X, by { ext, dsimp, simpa, }, }
 
 @[simp] lemma shift_functor_obj_apply {β : Type*} [add_comm_group β]
   (s : β) (X : β → C) (t : β) (n : ℤ) :