mathlib

c240fcb3 - feat(category_theory/limits): pullbacks from binary products and equalizers (#2143)

feat(category_theory/limits): pullbacks from binary products and equalizers (#2143) * feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y) * Rename *_of_diagram to diagram_iso_* * feat(category_theory/limits): pullbacks from binary products and equalizers * Fix build * Fix indentation * typos * Fix proof * Remove some simp lemmas that were duplicated during merge Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>