feat: add Function.{prod,diag,fstComp,sndComp,prodMap}

[linesthatinterlace]

Adds Mathlib/Logic/Function/Init.lean, centralising a cluster of general-purpose function operations in the Function namespace:

• Function.dcomp (notation ∘') — dependent composition, moved here from Mathlib/Logic/Function/Defs.lean.
• Function.prod (notation ⋏) — pointwise pair of two (possibly dependent) functions, (f ▽ g) i = (f i, g i).
• Function.fstComp / Function.sndComp — the two components of a function valued in a product; inverse to Function.prod.
• Function.diag (notation △) — the diagonal a ↦ (a, a).
• Function.prodMap — dot-notation alias for Prod.map; collapses to Prod.map under simp so existing API applies unchanged.

Pi.prod is removed in favour of Function.prod (which is itself the dependent version); a deprecated alias is provided.

The file depends only on Mathlib.Init (and Batteries.Tactic.Alias for the deprecated alias) so it can be upstreamed to Batteries / core without pulling mathlib dependencies.

• depends on: [Merged by Bors] - fix: rename Pi.prod to Function.prod #38963

[github-actions]

PR summary 1b6244ba2a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Notation.Pi.Defs	71	69	-2 (-2.82%)

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 7097 files with changed transitive imports taking up over 317497 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff

+ comp_prod_comp
+ const_dcomp
+ const_of_prod
+ const_prod_const
+ dcomp_apply
+ dcomp_assoc
+ dcomp_const
+ dcomp_def
+ dcomp_eq_comp
+ dcomp_id
+ dcomp_prod_dcomp
+ diag
+ diag_apply
+ diag_comp
+ eq_diag_fst_of_fst_eq_snd
+ eq_diag_snd_of_fst_eq_snd
+ eq_prod_iff
+ fstComp
+ fstComp_apply
+ fstComp_diag
+ fstComp_mk
+ fstComp_mk_flip
+ fstComp_prod
+ fstComp_prod_sndComp
+ fstComp_sndComp_ext
+ fstComp_sndComp_ext_iff
+ fst_comp
+ fst_dcomp
+ fst_diag_eq_snd_diag
+ fst_prod_snd
+ id_dcomp
+ id_prod_id
+ injective_diag
+ leftInverse_uncurry_prod_fstComp_prod_sndComp
+ left_eq_of_prod_eq
+ map_comp_diag
+ map_comp_prod
+ prodMap
+ prodMap_apply
+ prodMap_comp
+ prodMap_eq_prod_map
+ prodMap_id
+ prod_comp
+ prod_dcomp
+ prod_def
+ prod_eq_iff
+ prod_inj
+ rightInverse_uncurry_prod_fstComp_prod_sndComp
+ right_eq_of_prod_eq
+ sndComp
+ sndComp_apply
+ sndComp_diag
+ sndComp_mk
+ sndComp_mk_flip
+ sndComp_prod
+ snd_comp
+ snd_dcomp
+ snd_prod_fst
+ swap_comp_diag
+ swap_comp_prod
+ swap_dcomp_prod
+ uncurry_prod_injective
+ uncurry_prod_surjective
+-- prod_fst_snd
-+- prod_snd_fst

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[SnirBroshi]

This looks very cool!

[linesthatinterlace]

On reflection I have now removed Pi.prod and unified the file so that Function.prod is the dependent definition. Seems to work fine.

[linesthatinterlace]

The large import thing here seems to just be importing Alias.

[fpvandoorn]

This PR does way too many unrelated things in one PR, and I object to some of these.

Moreover, many of these changes add new things to very basic files, without any discussion/received support via Zulip.

Please discuss these changes (new definitions, new notation) on Zulip first, and implement if there is some support. Also link to these Zulip discussions in the top comment.

• Why do we need both Function.Defs and Function.Init?
• Why do you introduce unscoped non-standard notation? These basic pieces of notation that are imported everywhere should be discussed on Zulip first. I am personally against adding them, since they're just not that important in Mathlib (if they're scoped I'll only weakly object).
• Do we really need fstComp and sndComp? You might think that this is a nice "standardization" but it will just lead to https://xkcd.com/927/
  If it's useful for e.g. automation, start a discussion on Zulip and give compelling reasons there.
• What is the purpose of e.g. exists_fstComp? Suppose we want this result, why is it not written using Function.Surjective? exists_pair_prod also doesn't seem useful. Such results are best added when there is an actual need for them.
• Renaming Pi.prod -> Function.prod. This seems good, since it allows for dot notation f.prod g. I'd be happy to review a PR doing just this.

I think the best way forward is to close this PR, and make separate PRs for the pieces (after general Zulip approval).

[linesthatinterlace]

My intention was not to have this merged without Zulip discussion, but I wanted to get it to a state where I felt that it was ready for discussion. I suppose I should have marked this WIP to make that clear, but I wasn't sure if that label was still used. I'll start a thread there soon. The original motivation was that I keep wanting a compact notation for Function.prod (what is currently Pi.prod) and Function.diag.

[fpvandoorn]

Yes, the WIP tag is still used.
If there is no tag saying otherwise, we assume a PR is looking for someone to review it. You can remove the WIP tag by typing -WIP as a comment.
Thanks for starting the Zulip discussion.

[linesthatinterlace]

Ah, I think fundamentally I thought that PRs were considered WIP until active review was sought. I'll make sure my other ones reflect that.

[grunweg]

Ah, I think fundamentally I thought that PRs were considered WIP until active review was sought. I'll make sure my other ones reflect that.

That used to be the case (and many new contributors' PRs were sitting not-on-the-queue because of the opposite misunderstanding). In July 2024, the default was changed.
(You can also mark PRs as draft; that's another way to do the same thing.)

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - fix: rename Pi.prod to Function.prod #38963
  By Dependent Issues (🤖). Happy coding!