mathlib

94fc87ee - feat(category_theory/groupoid/free): functoriality of the free groupoid plus some cleanup (#16907)

feat(category_theory/groupoid/free): functoriality of the free groupoid plus some cleanup (#16907) Add lemmas witnessing functoriality of the free groupoid construction, and clean up some style/doc issues. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>