!4#2482 Bicategory.Free

Stream: mathlib4

[Scott Morrison]

I just did a fair bit of unsticking !4#2482 CategoryTheory.Bicategory.Free, which is critical for getting moving on monoidal categories (which I hope will be useful for homological algebra, sheaves of modules, etc etc.), but I am not quite there. If anyone is able to have a look that would be lovely.

It is failing on some proofs where in mathlib3 tidy just blasted through using induction, but I can't even do the inductions by hand here.

[Scott Morrison]

@Moritz Firsching, @Yuma Mizuno?

[Matthew Ballard]

It builds now

[Scott Morrison]

Fantastic. I always like it when the solution to be not being to prove something is to delete the relevant proof. :-)

[Matthew Ballard]

But you had already proven it. I asked tidy how they were done ;). Then filled in what steps aesop_cat couldn’t. In this case, it was the calls to Quot.rec