Commit 2026-08-13 09:18 6ee17e62

chore(CategoryTheory/Functor/Category): don't expose NatTrans.hcomp (#40925) This PR hides the definition of NatTrans.hcomp, because it has two equally sensible possible definitions. As a result, we can get rid of the to_dual_insert_cast. simps doesn't work for non-exposed definition, so hcomp_app is proved separately, and its dual hcomp_app' is added. Note: some proofs break, because the dsimp set changes, due to the definition not being exposed. This is a bit unfortunate. There was some discussion on Zulip about changing dsimp for category theory into a simp set, which would fix this problem, because we could then add hcomp_app to this set.