Some lemmas in mathlib could be global pull lemmas, but we would not like them as push lemmas: Function.comp_def is such an example. As a pull lemma, it expands g ∘ f to fun x => g (f x); there is no apparent use for the converse.
This appears when using the to_fun attribute to generate eta-expanded versions of some statements: in a number of places, we do attribute [local push ←] Function.comp_def to make to_fun behave the way we want. All these locations could benefit from this feature.
Some lemmas in mathlib could be global
pulllemmas, but we would not like them aspushlemmas:Function.comp_defis such an example. As a pull lemma, it expandsg ∘ ftofun x => g (f x); there is no apparent use for the converse.This appears when using the
to_funattribute to generate eta-expanded versions of some statements: in a number of places, we doattribute [local push ←] Function.comp_defto maketo_funbehave the way we want. All these locations could benefit from this feature.