Commit 2026-06-04 08:41 c87658ad

chore: use to_fun to auto-generated eta-expanded versions of comp declarations (#34361) Rename such declarations from comp' to fun_comp (as required by the naming convention) at the same time. In several cases, eta-expanding g ∘ f requires using Function.comp_def as pull lemma: as that lemma is not a push lemma, and there is no notion of global pull lemmas which are not push lemmas, we locally add the push attribute in reverse direction instead.