chore(category_theory): using simps#1500
Conversation
|
It'll be great to see the |
| end } | ||
|
|
||
| @[simp] lemma cone_point_a (D : J ⥤ algebra T) [has_limit.{v₁} (D ⋙ forget T)] : | ||
| (cone_point D).a = limit.lift _ ( |
There was a problem hiding this comment.
Was there a reason the old lemma was stated in such a way, not referring to c?
There was a problem hiding this comment.
Not that I've been able to work out... My best guess is that I was struggling with something that turned out to not be an issue, but I never cleaned up at the end, and it slipped through the PR process.
|
Did you have thoughts about the overlapping simp lemmas? My feeling is that I don't really know how bad they are, but the gain from using |
kim-em
added
awaiting-review
|
Okay, we may be good to go again, sorry about the delay. I've reverted all the overlapping simps. |
fpvandoorn
added
ready-to-merge
* chore(category_theory): using simps * more simps * remove simp lemma * revertings overlapping @[simps]
5 participants
Going through the category theory library and using
@[simps].I stopped partway through because I heard from @rwbarton that he'd also started to do this. I'll dump what I did here until we can coordinate.