chore(category_theory/monad): generate simp lemmas (#5972)

Adds a missing simps command to generate simp lemmas for the functor.
leanprover-community · Feb 1, 2021 · 8273588 · 8273588
1 parent 3f9b035
commit 8273588
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/category_theory/monad/products.lean b/src/category_theory/monad/products.lean
@@ -63,6 +63,7 @@ def over_to_coalgebra :
   map := λ f₁ f₂ g, { f := g.left } }
 
 /-- The equivalence from coalgebras for the product comonad to the over category. -/
+@[simps]
 def coalgebra_equiv_over :
   coalgebra (prod.functor.obj X) ≌ over X :=
 { functor := coalgebra_to_over X,