[Merged by Bors] - feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair by cameronfreer · Pull Request #34599 · leanprover-community/mathlib4

cameronfreer · 2026-01-30T05:08:58Z

Generalize Equiv.toCompl from [Finite α] to [Finite {x | p x}], which allows the target type to be infinite. In the process we add Perm.exists_extending_pair (given injections f, g : α → β for finite α, there is some σ : Perm β s.t. σ ∘ f = g) and Perm.exists_map_finset_eq.

This lets us simplifyPerm.isMultiplyPretransitive from 70 lines to 2 lines, avoiding cardinal arithmetic.

A version of this was used in formalizing de Finetti's theorem.

Co-authored-by: tb65536 tb65536@users.noreply.github.com

…ermutations Add lemmas for extending injective functions `Fin m → Fin n` to permutations of `Fin n`. - `Equiv.Perm.exists_extending_injective`: Any injective `k : Fin m → Fin n` extends to `σ : Perm (Fin n)` with `σ (Fin.castLE hmn i) = k i` - `Equiv.Perm.exists_extending_strictMono`: Special case for strictly monotone functions

Make docstrings more concise per mathlib style guidelines.

github-actions · 2026-01-30T05:10:09Z

PR summary 865d150803

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Perm.exists_extending_pair
+ Perm.exists_map_finset_eq
+ exists_smul_eq_embedding
+ setDiffEquiv

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./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/GroupTheory/Perm/Fin.lean

Use `Fin.le_of_injective` to derive `m ≤ n` automatically from the injectivity hypothesis, simplifying the API.

Mathlib/GroupTheory/Perm/Fin.lean

…emma Remove `Equiv.Perm.exists_extending_strictMono` since it's a trivial special case of `exists_extending_injective` (just apply `.injective`).

`Mathlib.Logic.Equiv.Fintype` is already imported transitively via `Cycle.Type` → `Cycle.Factors` → `Cycle.Basic` → `Perm.Finite`.

Mathlib/GroupTheory/Perm/Fin.lean

Add a general theorem stating that any two injective functions from a finite type to a finite type can be related by a permutation. This is the elementary form of the multiple pretransitivity of permutation groups (see `Equiv.Perm.isMultiplyPretransitive`).

Simplify `exists_extending_injective` to a one-line corollary of the new general `Perm.exists_extending_pair` theorem.

The `Finite β` constraint suffices since the ranges are subsets of `β`.

Mathlib/Logic/Equiv/Fintype.lean

…yPretransitive proof Use `Equiv.subtypeCongr` with `ofInjective` to build the permutation directly, eliminating the 57-line manual bijectivity proof via `Function.extend` and `Equiv.ofBijective`. The complement equivalence is still obtained via cardinal arithmetic.

…_extending_pair Add `Equiv.Perm.exists_extending_pair'` which generalizes `exists_extending_pair` from `[Finite β]` (target finite) to `[Finite α]` (source finite), using cardinal arithmetic for the complement equivalence. This allows the target type to be infinite. Use it to further simplify `isMultiplyPretransitive` to a 3-line proof.

The hypothesis is `[Finite β]` (target finite), not `[Finite α]`. Add cross-reference to the generalized `exists_extending_pair'`.

This was a one-line specialization of `exists_extending_pair` with no downstream uses. Callers can use `exists_extending_pair` directly. Also remove the now-unused `Mathlib.Data.Fin.Pigeonhole` import.

Rename `exists_extending_pair'` to `exists_extending_pair_of_finite_source` for discoverability, and add `exists_smul_eq_embedding` as the action-form wrapper. This reduces `isMultiplyPretransitive` to a two-line proof. Update cross-reference in `Fintype.lean` docstring accordingly.

…ite {x | p x}] Generalize `toCompl` and related definitions (`extendSubtype`, etc.) to only require finiteness of the subtype `{x | p x}` rather than the ambient type `α`. This allows `exists_extending_pair` to be strengthened from `[Finite β]` to `[Finite α]`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Replace 4 `grind` calls (experimental tactic) with stable alternatives: - Set identities: `ext; simp; tauto` - Disjointness: term-mode proof via `disjoint_compl_right.mono_left`

…f_finite_source Remove `exists_extending_pair_of_finite_source` which is now redundant since `Equiv.Perm.exists_extending_pair` has been generalized from `[Finite β]` to `[Finite α]`. Update `exists_smul_eq_embedding` to use `exists_extending_pair` directly.

mathlib-merge-conflicts · 2026-02-23T22:28:29Z

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

Keep our short `isMultiplyPretransitive` proof via `exists_smul_eq_embedding`, discarding the upstream grind-golfed version of the old long proof.

Mathlib/Logic/Equiv/Fintype.lean

Fix upstream regression in `extendSubtype_apply_of_not_mem` by using `simp only` + `rfl` instead of `simp`. Remove redundant `{α β : Type*}` from `Perm.exists_extending_pair` since they are already in scope.

riccardobrasca · 2026-03-31T08:52:47Z

Can we please have a human written PR description that says in a couple of lines what the PR does? It is currently almost as long as the diff. Thanks!

Mathlib/Logic/Equiv/Fintype.lean

Extract the finset sdiff cardinality argument from `toCompl` into `Equiv.setDiffEquiv`, and fix lint warnings in `Perm.exists_map_finset_eq`.

Mathlib/Logic/Equiv/Fintype.lean

riccardobrasca

#Thanks!

bors merge

…xists_extending_pair (#34599) Generalize `Equiv.toCompl` from `[Finite α]` to `[Finite {x | p x}]`, which allows the target type to be infinite. In the process we add `Perm.exists_extending_pair` (given injections `f, g : α → β` for finite `α`, there is some `σ : Perm β` s.t. `σ ∘ f = g`) and `Perm.exists_map_finset_eq`. This lets us simplify`Perm.isMultiplyPretransitive` from 70 lines to 2 lines, avoiding cardinal arithmetic. A [version of this](https://github.com/cameronfreer/exchangeability/blob/03a854a2/Exchangeability/Contractability.lean#L459) was used in formalizing de Finetti's theorem. Co-authored-by: tb65536 <tb65536@users.noreply.github.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-04-02T18:21:19Z

Pull request successfully merged into master.

Build succeeded:

cameronfreer added 2 commits January 29, 2026 23:45

style(GroupTheory/Perm/Fin): simplify docstrings for extension lemmas

4041858

Make docstrings more concise per mathlib style guidelines.

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory labels Jan 30, 2026

LLaurance reviewed Jan 30, 2026

View reviewed changes

Mathlib/GroupTheory/Perm/Fin.lean Outdated Show resolved Hide resolved

cameronfreer added 3 commits January 30, 2026 10:57

refactor(GroupTheory/Perm/Fin): derive m ≤ n from injectivity

736c074

Use `Fin.le_of_injective` to derive `m ≤ n` automatically from the injectivity hypothesis, simplifying the API.

style(GroupTheory/Perm/Fin): remove redundant docstrings

098a34e

doc(GroupTheory/Perm/Fin): mention agreement property in docstring

362b758

leanprover-community-bot-assistant assigned tb65536 Feb 3, 2026

tb65536 reviewed Feb 3, 2026

View reviewed changes

Mathlib/GroupTheory/Perm/Fin.lean Outdated Show resolved Hide resolved

tb65536 reviewed Feb 3, 2026

View reviewed changes

Mathlib/GroupTheory/Perm/Fin.lean Outdated Show resolved Hide resolved

tb65536 added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 3, 2026

cameronfreer added 2 commits February 3, 2026 19:07

chore(GroupTheory/Perm/Fin): remove StrictMono version of extension l…

b90cae9

…emma Remove `Equiv.Perm.exists_extending_strictMono` since it's a trivial special case of `exists_extending_injective` (just apply `.injective`).

chore(GroupTheory/Perm/Fin): remove redundant Fintype import

ea08732

`Mathlib.Logic.Equiv.Fintype` is already imported transitively via `Cycle.Type` → `Cycle.Factors` → `Cycle.Basic` → `Perm.Finite`.

tb65536 reviewed Feb 3, 2026

View reviewed changes

Mathlib/GroupTheory/Perm/Fin.lean Outdated Show resolved Hide resolved

cameronfreer added 4 commits February 3, 2026 21:13

refactor(GroupTheory/Perm/Fin): use exists_extending_pair

a5a7118

Simplify `exists_extending_injective` to a one-line corollary of the new general `Perm.exists_extending_pair` theorem.

golf(Logic/Equiv/Fintype): shorten exists_extending_pair proof

499e5d2

fix(Logic/Equiv/Fintype): remove unused Finite α hypothesis

2290eec

The `Finite β` constraint suffices since the ranges are subsets of `β`.

tb65536 reviewed Feb 3, 2026

View reviewed changes

Mathlib/Logic/Equiv/Fintype.lean Outdated Show resolved Hide resolved

cameronfreer and others added 9 commits February 17, 2026 16:45

docs(Logic/Equiv/Fintype): fix docstring for exists_extending_pair

6efac91

The hypothesis is `[Finite β]` (target finite), not `[Finite α]`. Add cross-reference to the generalized `exists_extending_pair'`.

chore(GroupTheory/Perm/Fin): remove exists_extending_injective

9c65ab6

This was a one-line specialization of `exists_extending_pair` with no downstream uses. Callers can use `exists_extending_pair` directly. Also remove the now-unused `Mathlib.Data.Fin.Pigeonhole` import.

[pre-commit.ci lite] apply automatic fixes

16b5c5b

golf(Logic/Equiv/Fintype): replace grind with term proofs in toCompl

ef7b66b

Replace 4 `grind` calls (experimental tactic) with stable alternatives: - Set identities: `ext; simp; tauto` - Disjointness: term-mode proof via `disjoint_compl_right.mono_left`

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 23, 2026

merge: resolve conflict with upstream master

f4a5fc8

Keep our short `isMultiplyPretransitive` proof via `exists_smul_eq_embedding`, discarding the upstream grind-golfed version of the old long proof.

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 23, 2026

mathlib-triage bot assigned mattrobball Feb 24, 2026

Merge branch 'master' into feat/perm-extend-injective-fin

906674e

tb65536 reviewed Mar 7, 2026

View reviewed changes

Mathlib/Logic/Equiv/Fintype.lean Outdated Show resolved Hide resolved

cameronfreer added 4 commits March 7, 2026 19:42

fix: repair extendSubtype_apply_of_not_mem proof and use variable scope

7fced4a

Fix upstream regression in `extendSubtype_apply_of_not_mem` by using `simp only` + `rfl` instead of `simp`. Remove redundant `{α β : Type*}` from `Perm.exists_extending_pair` since they are already in scope.

golf: simplify extendSubtype_mem and extendSubtype_apply_of_not_mem

bf75084

revert: keep convert/rw for extendSubtype_mem

df42b8c

Merge branch 'master' into feat/perm-extend-injective-fin

7694c32

mathlib-triage bot assigned riccardobrasca and unassigned mattrobball Mar 29, 2026

Merge branch 'master' into feat/perm-extend-injective-fin

fe83e6a

riccardobrasca reviewed Apr 1, 2026

View reviewed changes

Mathlib/Logic/Equiv/Fintype.lean Outdated Show resolved Hide resolved

cameronfreer added 2 commits April 2, 2026 01:52

refactor: extract setDiffEquiv and fix lint warnings

75f9bd2

Extract the finset sdiff cardinality argument from `toCompl` into `Equiv.setDiffEquiv`, and fix lint warnings in `Perm.exists_map_finset_eq`.

golf: simplify exists_map_finset_eq using eq_of_subset_of_card_le

fc2de20

cameronfreer changed the title ~~feat(Logic/Equiv/Fintype): generalize toCompl and exists_extending_pair to finite source~~ feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair Apr 2, 2026

riccardobrasca reviewed Apr 2, 2026

View reviewed changes

Mathlib/Logic/Equiv/Fintype.lean Outdated Show resolved Hide resolved

cameronfreer force-pushed the feat/perm-extend-injective-fin branch from 26ac0e1 to a424062 Compare April 2, 2026 14:38

style: convert toCompl from tactic mode to term mode

8691629

cameronfreer force-pushed the feat/perm-extend-injective-fin branch from a424062 to 8691629 Compare April 2, 2026 14:40

riccardobrasca reviewed Apr 2, 2026

View reviewed changes

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 2, 2026

mathlib-bors bot changed the title ~~feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair~~ [Merged by Bors] - feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair Apr 2, 2026

mathlib-bors bot closed this Apr 2, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair#34599

[Merged by Bors] - feat(Logic/Equiv/Fintype): generalize toCompl to finite source; add exists_extending_pair#34599
cameronfreer wants to merge 33 commits intoleanprover-community:masterfrom
cameronfreer:feat/perm-extend-injective-fin

cameronfreer commented Jan 30, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Jan 30, 2026 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Feb 23, 2026

Uh oh!

Uh oh!

riccardobrasca commented Mar 31, 2026

Uh oh!

Uh oh!

Uh oh!

riccardobrasca left a comment

Uh oh!

mathlib-bors bot commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

cameronfreer commented Jan 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 865d150803

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Feb 23, 2026

Uh oh!

Uh oh!

riccardobrasca commented Mar 31, 2026

Uh oh!

Uh oh!

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

cameronfreer commented Jan 30, 2026 •

edited

Loading

github-actions bot commented Jan 30, 2026 •

edited

Loading