[Merged by Bors] - feat(Data/List): Nodup and head & getLast lemmas

[Jun2M]

Given a Nodup list:

• If a prefix contains the last element, they are equal

• If a suffix contains the first element, they are equal

• If an infix contains the first element, it is a prefix

• If an infix contains the last element, it is a suffix

• If the first and the last element are the same, it is a singleton

• countP is cardinality of the filter of toFinset.

---

[github-actions]

PR summary 0927d675de

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ List.Nodup.card_eq_countP
+ Nodup.eq_of_getLast_mem_of_prefix
+ Nodup.eq_of_head_mem_of_getLast_mem_of_infix
+ Nodup.eq_of_head_mem_of_suffix
+ Nodup.head_eq_getLast_iff
+ Nodup.prefix_of_head_mem_of_infix
+ Nodup.suffix_of_getLast_mem_of_infix
+ filter_toFinset

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.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 0927d675de
Reference commit 783ccda4ee

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[joneugster]

Thank you for the PR!

[joneugster]

thank you!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[b-mehta]

This PR looks good to me, but I agree with Jon's point above.

[ocfnash]

I'd like a bit more thought about API here.

[joneugster]

Maybe it makes sense if I reassign this to @ocfnash for now. @Jun2M don't forget to comment -awaiting-author if this should be reviewed again.

[ocfnash]

I'm sorry to have been the cause of delaying this PR for so long.

Looking more closely now I retract my comment here as I now realise the moral duplication is a legacy of the fact that List.filter consumes a Bool-valued predicated whereas Finset.filter consumes a Prop-valued predicate. It's not pretty that we are in this situation and therefore have to author these morally duplicate lemmas (to enable convenient rewriting in each direction) but I do now agree that it is the best local action we can take.

Thanks for your patience.

[ocfnash]

@Jun2M I'll also repeat Jon's remark that you need to take action to get your PR back in the review queue or else it remains almost invisible to us.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job