1 files changed, 14 insertions, 6 deletions
diff --git a/Graded/GradedMonad.lean b/Graded/GradedMonad.lean
index d0af5f4..39d543c 100644
--- a/Graded/GradedMonad.lean
+++ b/Graded/GradedMonad.lean
@@ -54,17 +54,23 @@ def ofMonad (M : Monad C) : GradedMonad C where
   toFunctor _ := M.toFunctor
   η := M.η
   μ _ _ := M.μ
-  assoc X _ _ _ := by simp [M.assoc X]
-  left_unit X _ := by simp [M.left_unit]
-  right_unit X _ := by simp [M.right_unit]
+  assoc X _ _ _ := by simp only [Functor.comp_obj, eqToHom_refl, Category.comp_id]; exact M.assoc X
+  left_unit X _ := by simp only [eqToHom_refl, Category.comp_id]; exact M.left_unit X
+  right_unit X _ := by exact M.right_unit X
 
 def toMonad (M : GradedMonad C) : Monad C :=
   { M 0 with
     η := M.η
     μ := M.μ 0 0
-    assoc X := by simp [M.assoc X 0 0 0]
-    left_unit X := by simp [M.left_unit X 0]
-    right_unit X := by simp [M.right_unit X 0] }
+    assoc X := by
+      have h := M.assoc X 0 0 0
+      simp only [Functor.comp_obj, Nat.add_zero, eqToHom_refl, Category.comp_id] at h
+      exact h
+    left_unit X := by
+      have h := M.left_unit X 0
+      simp only [Functor.id_obj, Nat.add_zero, eqToHom_refl, Category.comp_id] at h
+      exact h
+    right_unit X := M.right_unit X 0 }
 
 lemma toMonad_ofMonad {M : Monad C} : (ofMonad M).toMonad = M := rfl
 
@@ -83,6 +89,8 @@ def ofComp (F : C ⥤ C) : GradedMonad C where
   η := NatTrans.id (𝟭 C)
   μ n k := NatTrans.id (compFunctor F k ⋙ compFunctor F n) ≫ eqToHom (compFunctor_comp _ n k)
   assoc X n k m := by simp [eqToHom_map]
+  left_unit X n := by simp [compFunctor]
+  right_unit X n := by simp [compFunctor]
 
 end GradedMonad