dcomp, Pi.map?

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#Function.dcomp which is used only a few times across the library. What do you think about replacing it with a bit less generic

@[inline]
def Pi.map {ι : Sort*} {α β : ι → Sort*} (f : ∀ i, α i → β i) (g : ∀ i, α i) : ∀ i, β i :=
  fun i ↦ f i (g i)

so that lemmas like docs#Function.surjective_pi_map can be formulated as |- Surjective (F ∘' ·) (if we keep notation) or |- Surjective (Pi.map F) (w/o notation)?

[Yury G. Kudryashov]

With current definition, (F ∘' ·) fails to elaborate.

[Yury G. Kudryashov]

More details: (F _ ∘' ·) elaborates if the type is known.

[Yury G. Kudryashov]

See #15694 and #15744 for context

[Yury G. Kudryashov]

UPD: making dcomp less dependent doesn't work with usage in docs#MeasureTheory.lmarginal_image