feat: lint for use of ellipsis

[menon-codes]

See the conversation at #mathlib4 > Linter for ellipsis @ 💬

Creates a linter to detect excessive use of _ holes at end of lemmas and replace it when appropriate with uses of ..

It also creates a respective test file to check it, though I am not too certain about the styles and techniques mathlib uses for testing.

AI (GPT 5.6 Terra) was used heavily in the documentation and testing of the code. Most of the logic and coding was done manually.

[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 a2746c59d9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8242 files with changed transitive imports taking up over 359557 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 (regex)

+ AppArgAnalysis
+ AppCandidate
+ analyzeApp?
+ analyzeAppArgs
+ appArgsLeaveFunctionCodomain
+ applyAllRewrites
+ batchFn
+ candidateRangeKey
+ collectValidatedRewrites
+ ellipsisPlaceholdersLinter
+ ellipsisTestFn
+ ellipsisTestFnAuto
+ ellipsisTestFnFour
+ ellipsisTestFnOpt
+ exprIsLambda
+ foldInfoM
+ fourArg
+ instBatch
+ instFn
+ isHoleArg
+ isInteractiveCommandDecl
+ isNamedArg
+ isSyntheticHole
+ lintCandidatesFromTree
+ markerBeforeTermKind
+ mathlibStyleThree
+ mathlibStyleWithMid
+ mixedTail
+ mkEllipsis
+ pipeWrap
+ rejectsPartialApplication
+ replacementAllowed
+ replacementIsSafe
+ rewriteApp
+ rewriteStopPos
+ shouldSkipValidation
+ sixArg
+ skippedContextKinds
+ splitAppArgs
+ syntaxRangesMatch
+ termInfoMatchesCandidate
+ traceSkip
+ tryLintCandidate
+ univFn
+ validateCommandWithAllRewrites
+ whnfIfScoped

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)

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

• +4 new declarations
• −0 removed declarations

+Mathlib.Linter.Style.ellipsisPlaceholders.«command#guard_ellipsis_rewrites_»
+Mathlib.Linter.linter.style.ellipsisPlaceholders
+Mathlib.Linter.linter.style.ellipsisPlaceholders.minTrailingHoles
+Mathlib.Linter.linter.style.ellipsisPlaceholders.trace

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a2746c59d9
Reference commit 30696563ac

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

[menon-codes]

LLM-generated

[menon-codes]

t-linter

[Copilot]

Pull request overview

This PR introduces a new style linter (ellipsisPlaceholders) that detects function applications ending in a long run of trailing _ placeholders and suggests replacing them with .., along with a dedicated test suite and wiring the linter into Mathlib’s linter imports.

Changes:

• Added Mathlib.Tactic.Linter.EllipsisPlaceholders: a syntax/infotree-based linter that validates and suggests rewriting trailing _ _ … to .. when safe.
• Added MathlibTest/Linter/EllipsisPlaceholders.lean to exercise expected warnings/non-warnings and rewrite validation.
• Updated Mathlib/Init.lean to import the new linter, and adjusted a lemma in NoetherNormalization to use a more direct integrality lemma.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

File	Description
Mathlib/Tactic/Linter/EllipsisPlaceholders.lean	New linter implementation and test helper command for validating bulk rewrites.
MathlibTest/Linter/EllipsisPlaceholders.lean	New regression / behavior tests for the linter’s warnings and skip cases.
Mathlib/RingTheory/NoetherNormalization.lean	Small proof refactor using an existing integrality lemma (.kerLift).
Mathlib/Init.lean	Adds the new linter module to the standard linter import set.

Suppressed comments (1)

Mathlib/Tactic/Linter/EllipsisPlaceholders.lean:526

• tryLintCandidate calls shouldSkipValidation even though replacementAllowed already performs the same check. After moving the trace message into replacementAllowed, this local check becomes redundant and does duplicate work on every candidate.

    if ← shouldSkipValidation ctx lctx ti then
      traceSkip "ellipsisPlaceholders: skipped application (unresolved metavariables in declaration body)"
      return false
    let suggested := rewriteApp c

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

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