fix(ProfiniteGrp): simplify explicit limit projections

[ashebson]

The naturality proof for ProfiniteCompletion.lift previously needed a brittle pointwise change. The underlying problem was that simplification crossed several semireducible diagram/forgetful-functor boundaries at once, producing terms that are definitionally equal but no longer type-correct at implicit transparency.

This PR:

• makes the two finite-quotient diagram composites reducible abbreviations;
• states quotientMap using the diagram object types and maps it through the existing FiniteGrp ⥤ ProfiniteGrp forgetful functor;
• adds a pointwise simp lemma for an explicit limit projection followed by a mapped finite-group morphism (with its additive counterpart); and
• rewrites ProfiniteCompletion.lift naturality through that API while keeping the limit point bundled, removing the problematic pointwise change.

---

AI disclosure

AI (OpenAI Codex) was used extensively for this PR. It was used to:

• investigate the original TODO and reproduce why dsimp failed;
• explore and discard several possible fixes;
• identify the semireducible diagram/forgetful-functor boundaries involved;
• design and implement the final ProfiniteGrp API simplification and ProfiniteCompletion.lift proof changes;
• run the relevant Lean builds and direct compilation checks; and
• draft the commit message and PR description.

The final changes were reviewed through the resulting diff and verified locally.

[github-actions]

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]

PR summary f63edb52e3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ limitCone_π_forget₂_map_apply
++-- diagram

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 -- stale, waiting for the new build)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9c6e697).

• +2 new declarations
• −0 removed declarations

+ProfiniteAddGrp.limitCone_π_forget₂_map_apply
+ProfiniteGrp.limitCone_π_forget₂_map_apply

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit f63edb52e3
Reference commit d7f2dbea7d

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-bors]

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.

[grunweg]

Hello from the triage team! Can you comment on whether you used AI for this project? Thanks!
Per mathlib's AI policy, this is not forbidden - but if you used AI, you must disclose that and how you used it.

[ashebson]

AI (OpenAI Codex) was used extensively for this PR. It was used to:

• investigate the original TODO and reproduce why dsimp failed;
• explore and discard several possible fixes;
• identify the semireducible diagram/forgetful-functor boundaries involved;
• design and implement the final ProfiniteGrp API simplification and ProfiniteCompletion.lift proof changes;
• run the relevant Lean builds and direct compilation checks; and
• draft the commit message and PR description.

The final changes were reviewed through the resulting diff and verified locally with lake build Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion (1892 jobs), direct compilation of Completion.lean, and git diff --check.

[ashebson]

@grunweg Thanks — I’ve added the requested AI-use disclosure above. Is anything else needed from me, or can the awaiting-author label be removed?

[grunweg]

Per the AI policy, the AI disclosure should be mentioned in the PR description (and this PR labelled LLM-generated). Can you do so, please? (While you're at it, please also take a look at the commit message guidelines. For instance, the entire "tested with" part is superfluous.) Thanks!

Once you have done this, you can comment -awaiting-author to remove that label.

[ashebson]

Thanks — done. I added the AI disclosure to the PR description and removed the Tested with section after reviewing the title and description guidelines.

LLM-generated
-awaiting-author