Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-18 19:41 05102ecb

View on Github →

chore(category_theory): using simps (#1500)

chore(category_theory): using simps
more simps
remove simp lemma
revertings overlapping @[simps]

Estimated changes

Modified src/category_theory/limits/cones.lean

modified def category_theory.cocones

deleted theorem category_theory.cocones_map

deleted theorem category_theory.cocones_obj

modified def category_theory.cones

deleted theorem category_theory.cones_map

deleted theorem category_theory.cones_obj

modified def category_theory.limits.cocone.whisker

deleted theorem category_theory.limits.cocone.whisker_ι_app

deleted theorem category_theory.limits.cocones.comp.hom

modified def category_theory.limits.cocones.ext

deleted theorem category_theory.limits.cocones.ext_hom_hom

modified def category_theory.limits.cocones.forget

deleted theorem category_theory.limits.cocones.forget_map

deleted theorem category_theory.limits.cocones.forget_obj

modified def category_theory.limits.cocones.functoriality

deleted theorem category_theory.limits.cocones.id.hom

modified def category_theory.limits.cocones.precompose

deleted theorem category_theory.limits.cocones.precompose_map_hom

deleted theorem category_theory.limits.cocones.precompose_obj_X

deleted theorem category_theory.limits.cocones.precompose_obj_ι

modified def category_theory.limits.cone.whisker

deleted theorem category_theory.limits.cone.whisker_π_app

deleted theorem category_theory.limits.cones.comp.hom

modified def category_theory.limits.cones.ext

deleted theorem category_theory.limits.cones.ext_hom_hom

modified def category_theory.limits.cones.forget

deleted theorem category_theory.limits.cones.forget_map

deleted theorem category_theory.limits.cones.forget_obj

modified def category_theory.limits.cones.functoriality

deleted theorem category_theory.limits.cones.id.hom

modified def category_theory.limits.cones.postcompose

deleted theorem category_theory.limits.cones.postcompose_map_hom

deleted theorem category_theory.limits.cones.postcompose_obj_X

deleted theorem category_theory.limits.cones.postcompose_obj_π

Modified src/category_theory/limits/functor_category.lean

modified def category_theory.limits.functor_category_colimit_cocone

modified def category_theory.limits.functor_category_limit_cone

Modified src/category_theory/limits/over.lean

modified def category_theory.functor.to_cocone

deleted theorem category_theory.functor.to_cocone_X

deleted theorem category_theory.functor.to_cocone_ι

modified def category_theory.functor.to_cone

deleted theorem category_theory.functor.to_cone_X

deleted theorem category_theory.functor.to_cone_π

modified def category_theory.over.colimit

deleted theorem category_theory.over.colimit_X_hom

deleted theorem category_theory.over.colimit_ι_app

modified def category_theory.under.limit

deleted theorem category_theory.under.limit_X_hom

deleted theorem category_theory.under.limit_π_app

Modified src/category_theory/monad/adjunction.lean

Modified src/category_theory/monad/algebra.lean

deleted theorem category_theory.monad.algebra.comp_f

modified def category_theory.monad.algebra.hom.comp

deleted theorem category_theory.monad.algebra.hom.comp_f

modified def category_theory.monad.algebra.hom.id

deleted theorem category_theory.monad.algebra.hom.id_f

deleted theorem category_theory.monad.algebra.id_f

modified def category_theory.monad.forget

deleted theorem category_theory.monad.forget_map

modified def category_theory.monad.free

deleted theorem category_theory.monad.free_map_f

deleted theorem category_theory.monad.free_obj_a

Modified src/category_theory/monad/limits.lean

modified def category_theory.monad.forget_creates_limits.c

deleted theorem category_theory.monad.forget_creates_limits.c_π

modified def category_theory.monad.forget_creates_limits.cone_point

deleted theorem category_theory.monad.forget_creates_limits.cone_point_a

modified def category_theory.monad.forget_creates_limits.γ

deleted theorem category_theory.monad.forget_creates_limits.γ_app

Modified src/category_theory/monoidal/functor.lean

modified def category_theory.lax_monoidal_functor.comp

deleted theorem category_theory.lax_monoidal_functor.comp_map

deleted theorem category_theory.lax_monoidal_functor.comp_obj

deleted theorem category_theory.lax_monoidal_functor.comp_ε

deleted theorem category_theory.lax_monoidal_functor.comp_μ

modified def category_theory.monoidal_functor.id

deleted theorem category_theory.monoidal_functor.id_map

deleted theorem category_theory.monoidal_functor.id_obj

deleted theorem category_theory.monoidal_functor.id_ε

deleted theorem category_theory.monoidal_functor.id_μ

Modified src/category_theory/whiskering.lean

modified def category_theory.functor.associator

deleted theorem category_theory.functor.associator_hom_app

deleted theorem category_theory.functor.associator_inv_app

modified def category_theory.functor.left_unitor

deleted theorem category_theory.functor.left_unitor_hom_app

deleted theorem category_theory.functor.left_unitor_inv_app

modified def category_theory.functor.right_unitor

deleted theorem category_theory.functor.right_unitor_hom_app

deleted theorem category_theory.functor.right_unitor_inv_app

Modified src/category_theory/yoneda.lean

deleted theorem category_theory.coyoneda.map_app

deleted theorem category_theory.coyoneda.obj_map

deleted theorem category_theory.coyoneda.obj_obj

modified def category_theory.coyoneda

deleted theorem category_theory.yoneda.map_app

deleted theorem category_theory.yoneda.obj_map

deleted theorem category_theory.yoneda.obj_obj

modified def category_theory.yoneda