Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-13 20:00 c8a0bb6b

View on Github →

feat(category_theory/products): missing simp lemmas (#1003)

feat(category_theory/products): missing simp lemmas
cleanup proofs
fix proof
squeeze_simp

Estimated changes

Modified src/category_theory/products/default.lean

modified def category_theory.evaluation

added theorem category_theory.evaluation_map_app

added theorem category_theory.evaluation_obj_map

added theorem category_theory.evaluation_obj_obj

modified def category_theory.evaluation_uncurried

added theorem category_theory.evaluation_uncurried_map

added theorem category_theory.evaluation_uncurried_obj

modified theorem category_theory.functor.prod_map

modified theorem category_theory.functor.prod_obj

added theorem category_theory.prod.fst_map

added theorem category_theory.prod.fst_obj

added theorem category_theory.prod.inl_map

added theorem category_theory.prod.inl_obj

added theorem category_theory.prod.inr_map

added theorem category_theory.prod.inr_obj

added theorem category_theory.prod.snd_map

added theorem category_theory.prod.snd_obj

added theorem category_theory.prod.swap_map

added theorem category_theory.prod.swap_obj