Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 09:27 037821b8

View on Github →

chore(category_theory/limits/types): remove simp lemmas (#3604) No one wants to see how the sausage is being made. Or at least, no one wants simp to show you without asking.

Estimated changes

Modified src/category_theory/limits/types.lean

modified theorem category_theory.limits.types.types_colimit

modified theorem category_theory.limits.types.types_colimit_desc

modified theorem category_theory.limits.types.types_colimit_map

modified theorem category_theory.limits.types.types_colimit_pre

modified theorem category_theory.limits.types.types_colimit_ι

modified theorem category_theory.limits.types.types_limit

modified theorem category_theory.limits.types.types_limit_lift

modified theorem category_theory.limits.types.types_limit_map

modified theorem category_theory.limits.types.types_limit_pre

modified theorem category_theory.limits.types.types_limit_π