Commit 2024-10-21 14:58 69a4014a

chore(CategoryTheory/Adjunction): homEquiv_unit is no longer a global simp lemma (#17761) This PR removes the global simp attribute to lemmas homEquiv_unit and homEquiv_counit. These lemmas express the bijection homEquiv in terms of the unit and counit of the adjunction. In situations where adjunctions are defined using the constructor mkOfHomEquiv, we do not want these lemmas as global simp. However, when we study adjunctions defined using units and counits, or when proving general API results about them, they can be made local simp.