CategoryTheory.Adjunction.Opposites !4#2424

Stream: mathlib4

[Adam Topaz]

I started porting this file in !4#2424 but it seems like a lot of simp lemmas are simply not firing. I also had to resort to erw in some places which is really not ideal. I don't have time to diagnose these issues right now, so any help getting this file in shape (preferably with proofs that are as short as those from mathlib3) would be great!

[Adam Topaz]

Oh, and I still haven't fixed a good number of the proofs, so there are still a good number of sorries in this branch