mathlib3

f1bf7b87 - feat(category_theory/filtered): Special support for bowtie and tulip diagrams (#9099)

feat(category_theory/filtered): Special support for bowtie and tulip diagrams (#9099) Add special support for two kinds of diagram categories: The "bowtie" and the "tulip". These are convenient when proving that forgetful functors of algebraic categories preserve filtered colimits. Co-authored-by: Johan Commelin <johan@commelin.net>