Commit 2020-09-03 11:22 fa6485a5

View on Github →

feat(category_theory/limits/concrete): simp lemmas (#3973) Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently.

Estimated changes

Modified src/algebra/category/Group/limits.lean

deleted theorem AddCommGroup.lift_π_apply

Modified src/category_theory/concrete_category/basic.lean

Modified src/category_theory/limits/concrete_category.lean

deleted theorem category_theory.limits.cocone.naturality_concrete

added theorem category_theory.limits.cocone.w_apply

added theorem category_theory.limits.cocone.w_forget_apply

added theorem category_theory.limits.colimit.w_apply

added theorem category_theory.limits.colimit.ι_desc_apply

deleted theorem category_theory.limits.cone.naturality_concrete

added theorem category_theory.limits.cone.w_apply

added theorem category_theory.limits.cone.w_forget_apply

added theorem category_theory.limits.limit.lift_π_apply

added theorem category_theory.limits.limit.w_apply