Commit 2024-08-26 15:01 501c8332
View on Github →chore(CategoryTheory/Adjunction): clean up file Adjunction.Basic (#16071)
Removes a bunch of porting notes and simplifies some proofs.
Also removes the simp attributes from the homEquiv_naturality lemmas. These were bad simp lemmas because they can interfere with the simp lemmas homEquiv_unit and homEquiv_counit. Removing them doesn't break anything throughout all of mathlib.