mathlib

2065438d - feat(category_theory/comma): some limits in the over category and iterated slices (#2131)

feat(category_theory/comma): some limits in the over category and iterated slices (#2131) * iterated slice and limits in over category * A bit more docs * changes from review * removed simp attributes * over prod map left * Update src/category_theory/comma.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * simplify equivalence definition * fix indentation * make lemmas simp again * removed simp * fix equalizers proof Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>