Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-04 07:43 2d00ba48

View on Github →

feat(category_theory/limits): cleanup equalizers (#5214) golf and make simp more powerful

Estimated changes

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

deleted theorem category_theory.limits.cocone_of_split_epi_ι_app_one

deleted theorem category_theory.limits.cocone_of_split_epi_ι_app_zero

modified theorem category_theory.limits.cofork.condition

modified theorem category_theory.limits.cofork.π_eq_app_one

modified theorem category_theory.limits.cofork.π_of_π

deleted theorem category_theory.limits.cone_of_split_mono_π_app_one

deleted theorem category_theory.limits.cone_of_split_mono_π_app_zero

modified theorem category_theory.limits.fork.condition

modified theorem category_theory.limits.fork.ι_eq_app_zero

modified theorem category_theory.limits.fork.ι_of_ι

modified def category_theory.limits.split_epi_coequalizes