Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-26 08:05 59382264

View on Github →

refactor(category_theory/*): use simps in the old parts of the library (#14236)

Estimated changes

Modified src/algebraic_topology/cech_nerve.lean

Modified src/category_theory/functor/basic.lean

modified def category_theory.functor.comp

deleted theorem category_theory.functor.comp_obj

Modified src/category_theory/functor/category.lean

deleted theorem category_theory.functor.flip_map_app

deleted theorem category_theory.functor.flip_obj_map

deleted theorem category_theory.functor.flip_obj_obj

modified def category_theory.nat_trans.hcomp

deleted theorem category_theory.nat_trans.hcomp_app

Modified src/category_theory/functor/const.lean

deleted theorem category_theory.functor.const.map_app

deleted theorem category_theory.functor.const.obj_map

deleted theorem category_theory.functor.const.obj_obj

modified def category_theory.functor.const.op_obj_op

deleted theorem category_theory.functor.const.op_obj_op_hom_app

deleted theorem category_theory.functor.const.op_obj_op_inv_app

modified def category_theory.functor.const

Modified src/category_theory/functor/currying.lean

deleted theorem category_theory.curry.map_app_app

deleted theorem category_theory.curry.obj_map_app

deleted theorem category_theory.curry.obj_obj_map

deleted theorem category_theory.curry.obj_obj_obj

deleted theorem category_theory.uncurry.map_app

deleted theorem category_theory.uncurry.obj_map

deleted theorem category_theory.uncurry.obj_obj

Modified src/category_theory/functor/hom.lean

added def category_theory.functor.hom

deleted theorem category_theory.functor.hom_obj

deleted theorem category_theory.functor.hom_pairing_map

Modified src/category_theory/limits/colimit_limit.lean

Modified src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean

Modified src/category_theory/limits/final.lean

Modified src/category_theory/limits/fubini.lean

Modified src/category_theory/limits/shapes/equalizers.lean

Modified src/category_theory/natural_isomorphism.lean

deleted theorem category_theory.nat_iso.of_components.hom_app

deleted theorem category_theory.nat_iso.of_components.inv_app

modified def category_theory.nat_iso.of_components

Modified src/category_theory/sites/left_exact.lean

Modified src/category_theory/structured_arrow.lean

Modified src/group_theory/nielsen_schreier.lean

Modified src/topology/category/CompHaus/default.lean

Modified src/topology/sheaves/presheaf.lean

Modified src/topology/sheaves/sheaf_condition/equalizer_products.lean