chore(Combinatorics/SimpleGraph/Copy): replace classical `Fintype.card` with `Nat.card` by FordUniver · Pull Request #38931 · leanprover-community/mathlib4

FordUniver · 2026-05-04T13:00:28Z

Replaces definitions of copyCount and unlabeledCopyCount with Nat.card instead of Fintype.card as well as several Fintype occurrences with Finite. The body of uniqueUnlabeledCopyBot is restructured to use Finite.injective_iff_surjective since the Fintype.card_congr route no longer applies under the weakened [Finite W] hypothesis. Adds public copyCount_eq_nat_card and unlabeledCopyCount_eq_nat_card bridge lemmas so downstream files can characterize the counts (e.g. for Nat.card_le_card_of_injective bridging in InducedCopy.lean) without unfolding.

Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com

Step 4/5 of the Copy / InducedCopy refactor-feat stack.

As suggested in #38631 by @SnirBroshi and @YaelDillies. I went with Nat over ENat based on Yael's preference (but I think that could easily be changed to ENat). Quite a bit of churn was needed as a consequence.

depends on: chore(Combinatorics/SimpleGraph/Copy): replace file-wide @[expose] with selective exposure #38843

Diff for the changes just in this PR over its predecessor: link

github-actions · 2026-05-04T13:00:40Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-05-04T13:01:36Z

PR summary dab7855eae

Import changes exceeding 2%

%	File
+29.72%	`Mathlib.Combinatorics.SimpleGraph.Copy`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Copy	599	777	+178 (+29.72%)

Import changes for all files

Files	Import difference
13 files `Mathlib.Combinatorics.SimpleGraph.Circulant` `Mathlib.Combinatorics.SimpleGraph.Clique` `Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring` `Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex` `Mathlib.Combinatorics.SimpleGraph.Coloring` `Mathlib.Combinatorics.SimpleGraph.CycleGraph` `Mathlib.Combinatorics.SimpleGraph.Hasse` `Mathlib.Combinatorics.SimpleGraph.Partition` `Mathlib.Combinatorics.SimpleGraph.Prod` `Mathlib.Combinatorics.SimpleGraph.Sum` `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite`	1
`Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic`	59
`Mathlib.Combinatorics.SimpleGraph.Extremal.Basic`	99
`Mathlib.Combinatorics.SimpleGraph.Copy` `Mathlib.Combinatorics.SimpleGraph.LineGraph`	178

Declarations diff (regex)

+ UnlabeledCopy
+ copyCount_eq_nat_card
+ instance : FunLike (Copy G H) V W
+ instance : IsPreorder (SimpleGraph V) IsContained
+ instance : IsPreorder (SimpleGraph V) IsIndContained
+ instance [Finite V] [Finite W] : Finite (G.Copy H)
+ instance [Finite W] : Finite (G.UnlabeledCopy H) := Subtype.finite
+ instance [IsEmpty V] : Nonempty (Copy G H) := IsContained.of_isEmpty
+ instance [IsEmpty V] : Nonempty (G.UnlabeledCopy H)
+ instance [IsEmpty V] : Subsingleton (G.UnlabeledCopy H)
+ le_card_edgeFinset_killCopies_add_unlabeledCopyCount
+ toEmbedding_apply
+ topEmbedding_apply
+ uniqueUnlabeledCopyBot
+ unlabeledCopyCount
+ unlabeledCopyCount_bot
+ unlabeledCopyCount_eq_card_image_copyToSubgraph
+ unlabeledCopyCount_eq_nat_card
+ unlabeledCopyCount_eq_zero
+ unlabeledCopyCount_le_copyCount
+ unlabeledCopyCount_of_isEmpty
+ unlabeledCopyCount_pos
- copyCount_bot
- copyCount_le_labelledCopyCount
- instance : FunLike (Copy A B) α β
- instance : IsPreorder (SimpleGraph α) IsContained
- instance : IsPreorder (SimpleGraph α) IsIndContained
- le_card_edgeFinset_killCopies_add_copyCount

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.

Decrease in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5012	-1	exposed public sections

Current commit dab7855eae
Reference commit 47550252e7

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).

github-actions · 2026-05-04T13:01:47Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

mathlib-dependent-issues · 2026-05-04T13:33:55Z

This PR/issue depends on:

chore(Combinatorics/SimpleGraph/Copy): replace file-wide @[expose] with selective exposure #38843
By Dependent Issues (🤖). Happy coding!

SnirBroshi · 2026-05-13T13:58:02Z

I think the parts about copies should be split to a separate file to avoid the import increase.

mathlib-bors · 2026-05-13T15:00:41Z

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

mathlib-merge-conflicts · 2026-05-23T17:44:36Z

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

Adds `abbrev Sub A B := {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}`, the subtype of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. Redefines `copyCount G H` via `Fintype.card (H.Sub G)`, replacing the previous inline filter-set body, and rewrites the affected proofs (`copyCount_eq_zero`, `copyCount_pos`, `copyCount_le_labelledCopyCount`, `copyCount_bot`, `le_card_edgeFinset_killCopies`) to use `Sub` directly. The singleton-empty-subgraph reasoning previously inlined in `copyCount_bot`'s proof is factored out as `instance uniqueSubBot (G : SimpleGraph V) : Unique ((⊥ : SimpleGraph V).Sub G)`, making `copyCount_bot` a one-liner via `Fintype.card_unique`. The cardinality proof inside the instance stays inline to keep the introduction minimal — extraction to a separate private helper and the rename to `_emptyGraph` per the convention from leanprover-community#23838 (and adopted in `AdjMatrix.lean`) happen in the next PR. Drops `copyCount_eq_card_image_copyToSubgraph` (the legacy bridge between the filter-set and Finset.image-of-Copy.toSubgraph forms) — unused after the type-form refactor.

…copyToSubgraph as deprecated Restores the exact statement of the legacy bridge lemma dropped when copyCount was redefined via UnlabeledCopy, now carrying @[deprecated] (since 2026-07-12) per review, with a proof against the new Fintype.card (H.UnlabeledCopy G) body.

@SnirBroshi

…y graph variables Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H` (labelled, injective hom from `G` into `H`) is paired with the count `H.copyCount G` (labelled count, host-first per mathlib op convention) and the `UnlabeledCopy G H` carrier (introduced in the previous PR) is paired with the count `H.unlabeledCopyCount G`. Also unifies the graph-variable letters: the `A B C` set that was local to `Copy.lean` is dropped in favour of mathlib's wider `G H I` convention, with `α β γ` → `V W X` correspondingly. Within the new convention `G` is the guest (pattern, contained side) and `H` is the host (container), matching `G ⊑ H` and the hom direction `G →g H`. Types are guest-first (`Copy G H`, `UnlabeledCopy G H`); operations are host-first via dot notation (`H.copyCount G`, `H.unlabeledCopyCount G`, `H.killCopies G`). This matches the existing mathlib convention split (hom types use source-first, host-side operations use the host as the dot-notation receiver). Changes: * Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias `labelledCopyCount`). The previous `copyCount → unlabeledCopyCount` rename has no alias — `copyCount` is reassigned to mean the labelled count. Same for the `_of_isEmpty` / `_eq_zero` / `_pos` lemma families. * Rename `copyCount_bot → unlabeledCopyCount_bot` (count name rename only; `_bot` spelling preserved per @SnirBroshi). * Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names (`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`; primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the cross-universe variants used in `isContained_congr` / `free_congr` (and their `_left` / `_right` partial-iso forms). This preserves the universe polymorphism the old `A B C / α β γ` block provided implicitly and that `Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies on. * Fix the docstring direction on `IsContained.trans` and `.trans'`: the previous wording ("`G` contains `H`") read the relation backwards relative to the lemma signature (`G ⊑ H` means `G` is contained in `H`). * Update module docstring (`UnlabeledCopy` / `unlabeledCopyCount` bullets, logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and the three densities.

…th selective exposure Replace `@[expose] public section` with a plain `public section` and restore selective `@[expose]` on only the declarations that need cross-module reduction: * `Copy.toEmbedding`, `Copy.id`, `Copy.ofLE`, `Copy.topEmbedding` — the small constructive copy `def`s, kept transparent so consumers can elaborate against them by reducing. * `copyCount`, `subCount` — the noncomputable counts. These need to be exposed so downstream files (e.g. the upcoming `InducedCopy.lean` in feat/ind-copy-count) can prove bridging inequalities like `embCount_le_copyCount` and `indSubCount_le_subCount` directly via `Nat.card_le_card_of_injective`. Also: * Inline the `@[simps!]` projections of `Copy.topEmbedding` into a manual `@[simp] lemma topEmbedding_apply` (and similarly for `Copy.toEmbedding`). The auto-generated `simps` form attached to `@[simps!]` was opaque to cross-module simp; the manual form is small enough to ship as a one-line named lemma. The body of `topEmbedding` is also tightened from `fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, _⟩` to `fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, _⟩`. * `IsIndContained` switches from `def` to `abbrev`, since the body `Nonempty (G ↪g H)` is small and downstream Lean elaboration benefits from automatic unfolding here.

…yCount to Nat.card * `copyCount` and `unlabeledCopyCount` redefined via `Nat.card` instead of `Fintype.card`. * `Fintype` hypotheses weakened to `Finite` throughout (`copyCount_eq_zero`, `copyCount_pos`, `unlabeledCopyCount_eq_zero`, `unlabeledCopyCount_pos`, `unlabeledCopyCount_le_copyCount`, `uniqueUnlabeledCopyBot`, `unlabeledCopyCount_bot`, `unlabeledCopyCount_of_isEmpty`, `bot_isContained_iff_card_le`, `le_card_edgeFinset_killCopies`, `le_card_edgeFinset_killCopies_add_unlabeledCopyCount`). * `bot_isContained_iff_card_le`: `Fintype.card → Nat.card`. * New `Finite (G.Copy H)` instance (sibling to the existing `Fintype` instance). * New `Nonempty (Copy G H)` instance for `[IsEmpty V]`, used to give a one-line `copyCount_of_isEmpty` proof via `Nat.card_unique`. * New `copyCount_eq_nat_card` and `unlabeledCopyCount_eq_nat_card` bridge lemmas exposing the underlying `Nat.card`, intended as the public characterisation since the count bodies are deliberately not `@[expose]`d. * New private `Nonempty` / `Subsingleton` instances on `G.UnlabeledCopy H` for `[IsEmpty V]`, used to give a one-line `unlabeledCopyCount_of_isEmpty` proof via `Nat.card_unique`. * `le_card_edgeFinset_killCopies` proof simplified accordingly.

mathlib-merge-conflicts · 2026-07-17T01:00:23Z

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

…of of copyCount_le_labelledCopyCount

…definition

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 4, 2026

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label May 4, 2026

github-actions Bot added the t-combinatorics Combinatorics label May 4, 2026

FordUniver mentioned this pull request May 4, 2026

feat(Combinatorics/SimpleGraph/InducedCopy): add UnlabeledEmbedding, unlabeledEmbeddingCount and embeddingCount #38631

Open

2 tasks

FordUniver requested review from SnirBroshi and YaelDillies May 4, 2026 13:08

FordUniver changed the title ~~Chore/copy nat card~~ Chore (Combinatorics/SimpleGraph/Copy): replace classical Fintype.card with Nat.card May 4, 2026

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 4, 2026

FordUniver force-pushed the chore/copy-nat-card branch 3 times, most recently from ebfa4d7 to d20fe0f Compare May 4, 2026 15:26

FordUniver changed the title ~~Chore (Combinatorics/SimpleGraph/Copy): replace classical Fintype.card with Nat.card~~ chore(Combinatorics/SimpleGraph/Copy): replace classical Fintype.card with Nat.card May 4, 2026

FordUniver mentioned this pull request May 12, 2026

refactor(Combinatorics/SimpleGraph/Copy): rename copy counts, align variable names, clean up docstring #38745

Open

1 task

FordUniver force-pushed the chore/copy-nat-card branch 6 times, most recently from 6700ac2 to c5ac97f Compare May 13, 2026 13:05

FordUniver mentioned this pull request May 13, 2026

chore(Combinatorics/SimpleGraph/Copy): rename _bot lemmas to _emptyGraph #39303

Closed

FordUniver force-pushed the chore/copy-nat-card branch from c5ac97f to bc53277 Compare May 13, 2026 14:50

FordUniver marked this pull request as draft May 13, 2026 15:00

FordUniver force-pushed the chore/copy-nat-card branch 2 times, most recently from c6caa5c to ad9826f Compare May 13, 2026 16:22

FordUniver force-pushed the chore/copy-nat-card branch from 768edab to e6247f6 Compare May 25, 2026 07:10

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 May 25, 2026

FordUniver changed the title ~~chore(Combinatorics/SimpleGraph/Copy): replace classical Fintype.card with Nat.card~~ chore(Combinatorics/SimpleGraph/Copy): replace classical Fintype.card with Nat.card May 28, 2026

FordUniver added 2 commits June 13, 2026 21:10

Renamed Sub to UnlabeledCopy per suggestion by mitchell-horner

65fb74a

FordUniver force-pushed the chore/copy-nat-card branch 2 times, most recently from 204bcdc to 28e3a52 Compare June 13, 2026 20:16

YaelDillies removed their request for review July 1, 2026 06:12

FordUniver and others added 6 commits July 8, 2026 17:24

chore: fix stale Sub reference in UnlabeledCopy docstring

2b608ef

Merge branch 'master' into feat/copy-sub-abbrev

5699548

FordUniver force-pushed the chore/copy-nat-card branch from 28e3a52 to e7cb121 Compare July 12, 2026 02:21

github-actions Bot added the tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip label Jul 12, 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 Jul 17, 2026

FordUniver added 2 commits July 17, 2026 14:27

restored simpler proof of copyCount_eq_zero

dec7da1

un-deprecated copyCount_eq_card_image_copyToSubgraph and restored pro…

9a02a88

…of of copyCount_le_labelledCopyCount

FordUniver mentioned this pull request Jul 17, 2026

feat(Combinatorics/SimpleGraph/Copy): introduce UnlabeledCopy carrier subtype #39307

Open

FordUniver and others added 7 commits July 17, 2026 23:33

Merge branch 'master' into feat/copy-sub-abbrev

bf51685

Merge feat/copy-sub-abbrev into chore/copy-spelling

314f1f8

replace deprecated mem_setOf_eq with mem_ofPred_eq

40e1050

Merge updated feat/copy-sub-abbrev into chore/copy-spelling

4a320e8

Merge updated chore/copy-spelling into chore/copy-expose

cb0352f

chore(Combinatorics/SimpleGraph/Copy): make UnlabeledCopy an exposed …

1f67407

…definition

Merge updated chore/copy-expose into chore/copy-nat-card

dab7855

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 Jul 17, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

chore(Combinatorics/SimpleGraph/Copy): replace classical `Fintype.card` with `Nat.card`#38931

chore(Combinatorics/SimpleGraph/Copy): replace classical `Fintype.card` with `Nat.card`#38931
FordUniver wants to merge 17 commits into
leanprover-community:masterfrom
FordUniver:chore/copy-nat-card

FordUniver commented May 4, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 4, 2026

Uh oh!

github-actions Bot commented May 4, 2026 •

edited

Loading

Import changes for modified files

Declarations diff (regex)

Uh oh!

github-actions Bot commented May 4, 2026 •

edited

Loading

Uh oh!

mathlib-dependent-issues Bot commented May 4, 2026 •

edited

Loading

Uh oh!

SnirBroshi commented May 13, 2026

Uh oh!

mathlib-bors Bot commented May 13, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 23, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jul 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

FordUniver commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 4, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary dab7855eae

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- pending)

Uh oh!

github-actions Bot commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

mathlib-dependent-issues Bot commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SnirBroshi commented May 13, 2026

Uh oh!

mathlib-bors Bot commented May 13, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 23, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jul 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

FordUniver commented May 4, 2026 •

edited

Loading

github-actions Bot commented May 4, 2026 •

edited

Loading

github-actions Bot commented May 4, 2026 •

edited

Loading

mathlib-dependent-issues Bot commented May 4, 2026 •

edited

Loading