[Merged by Bors] - feat(Tactic): automatically replace convert with convert! by Vierkantor · Pull Request #39721 · leanprover-community/mathlib4

Vierkantor · 2026-05-22T20:02:31Z

This PR makes any use of convert pop up a "Try this:" message replacing it with convert!. This prepares for #39039 which will make convert change behaviour and convert! retain the old behaviour.

Note that convert and convert! still do the same thing and result in the same goals after this PR is applied, except convert! does not pop up a "Try this:" afterwards.

After the code in this PR passes an initial review, I will run Skimmer to apply all the "Try this:" messages.

depends on: [Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change! #39715

This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

This PR sets up an option for `congr!` to close generated goals with configurable transparency, but does not enable this by default. Then it adds a check to `convert` where it will run the `congr!` algorithm at both reducible and default transparency. In the case the default transparency generates different goals, it pops up a "Try this:" suggestion to use `convert!`. Applying all the "Try this:" suggestions to Mathlib means we can then change the semantics of `convert` to close the goals reducibly. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards.

github-actions · 2026-05-22T20:03:51Z

PR summary 5230f2468c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

No changes to strong technical debt.

No changes to weak technical debt.

grunweg · 2026-05-22T20:21:05Z

The replacement logic LGTM!

mathlib-dependent-issues · 2026-05-22T20:46:27Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change! #39715~~
By Dependent Issues (🤖). Happy coding!

Since antiquotations inside the `congr()` elaborator can't be pretty-printed reliably, manually change `convert congr(...)` to `convert! congr(...)`.

github-actions · 2026-05-22T23:15:49Z

Commit Verification Summary

Warning

Some verifications failed. See details below.

Commits to Review (15)

381a876: feat(Tactic): add syntax for convert!, convert_to!, ac_change!
7111187: Forgot a @[tactic_alt]
2de70d7: feat(Tactic): automatically replace convert with convert!
64c8460: Revert
0f5e8c5: Unconditionally suggest replacing convert with convert!
ea3e0c6: Undo most changes, just add exclamations to all converts
d068217: Manual fixes
ee2171d: Fixes
39f4323: Final fixes
60a7bd5: Merge remote-tracking branch 'upstream/master' into convert-to-bang
bc78238: [pre-commit.ci lite] apply automatic fixes
ff707b1: Fix the using and the number being put on separate lines
6f98e11: Fix merge
4e4a807: Disable the "Try this:" message
5230f24: Line length

View PR diff

❌ Automated commits (2) — 0/2 verified

❌ e9127aa: x ./scripts/runSkimmer.sh

Command exited with code 127.

Output:

Note: the functionality provided by this script is experimental and subject to change. This script will become unnecessary in the future.
Please report any issues (especially incomprehensible ones!) to Thomas Murrills on Zulip.
Running `lake update` in `SideSkimmer`. Use `runSkimmer.sh --no-update` to skip this step.
./scripts/runSkimmer.sh: line 131: lake: command not found
Note: `runSkimmer.sh` uses available oleans from the targeted package and builds necessary ones. Consider getting the cache prior to running if possible.
Running `lake build Mathlib:applyCurrentTryThis`.
./scripts/runSkimmer.sh: line 145: lake: command not found

❌ 7ab80cd: x ./scripts/runSkimmer.sh --on Archive Counterexamples MathlibTest

Command exited with code 127.

Output:

Note: the functionality provided by this script is experimental and subject to change. This script will become unnecessary in the future.
Please report any issues (especially incomprehensible ones!) to Thomas Murrills on Zulip.
Running `lake update` in `SideSkimmer`. Use `runSkimmer.sh --no-update` to skip this step.
./scripts/runSkimmer.sh: line 131: lake: command not found
Note: `runSkimmer.sh` uses available oleans from the targeted package and builds necessary ones. Consider getting the cache prior to running if possible.
Running `lake build Archive:applyCurrentTryThis`.
./scripts/runSkimmer.sh: line 145: lake: command not found
Running `lake build Counterexamples:applyCurrentTryThis`.
./scripts/runSkimmer.sh: line 145: lake: command not found
Running `lake build MathlibTest:applyCurrentTryThis`.
./scripts/runSkimmer.sh: line 145: lake: command not found

Generated by commit verification CI

grunweg · 2026-05-23T00:11:08Z

The current status is good: let's try merging this --- and if there's a conflict in the morning, we can re-do.
bors merge

This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for #39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-05-23T00:58:47Z

Build failed:

ci (staging) / Build

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

grunweg · 2026-05-23T08:12:17Z

Silly CI error (line length); it seems no merge conflicts yet.

grunweg · 2026-05-23T08:23:46Z

CI error is unrelated to this PR (I've just re-run): let's try if this can just be borsed.
bors merge

This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for #39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2026-05-23T09:01:36Z

Build failed:

ci (staging) / Post-CI job

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

grunweg · 2026-05-23T09:41:20Z

Once more, with feeling:
bors r+

This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for #39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2026-05-23T09:53:14Z

Pull request successfully merged into master.

Build succeeded:

grunweg · 2026-05-23T09:55:42Z

It worked 🎉

…-community#39721) This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for leanprover-community#39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

…-one Conflict in Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean caused by leanprover-community#39721 (convert → convert! rename). Resolved by keeping HEAD — our refactored `dimension_level_one` proof replaced the `convert; norm_num` block with `simpa [Nat.ModEq] using ...`, so the upstream rename doesn't apply. `QExpansion.lean` auto-merged cleanly; `convert` calls there are now `convert!` as intended. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…-community#39721) This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for leanprover-community#39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Vierkantor added 3 commits May 22, 2026 17:21

Forgot a @[tactic_alt]

7111187

Vierkantor requested a review from grunweg May 22, 2026 20:02

Vierkantor added the t-meta Tactics, attributes or user commands label May 22, 2026

Vierkantor mentioned this pull request May 22, 2026

feat(Tactic): convert now discharges side goals at reducible transparency #39039

Open

3 tasks

Vierkantor commented May 22, 2026

View reviewed changes

Comment thread Mathlib/Tactic/CongrExclamation.lean Outdated

Vierkantor and others added 3 commits May 22, 2026 21:05

Revert

64c8460

Unconditionally suggest replacing convert with convert!

0f5e8c5

Undo most changes, just add exclamations to all converts

ea3e0c6

Vierkantor force-pushed the convert-to-bang branch from 5340b1e to ea3e0c6 Compare May 22, 2026 20:19

grunweg self-assigned this May 22, 2026

Vierkantor added 2 commits May 22, 2026 22:18

Manual fixes

d068217

Since antiquotations inside the `congr()` elaborator can't be pretty-printed reliably, manually change `convert congr(...)` to `convert! congr(...)`.

x ./scripts/runSkimmer.sh

e9127aa

github-actions 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 May 22, 2026

Vierkantor added 4 commits May 23, 2026 00:06

Fixes

ee2171d

x ./scripts/runSkimmer.sh --on Archive Counterexamples MathlibTest

7ab80cd

Final fixes

39f4323

Merge remote-tracking branch 'upstream/master' into convert-to-bang

60a7bd5

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 22, 2026

[pre-commit.ci lite] apply automatic fixes

bc78238

Vierkantor added 3 commits May 23, 2026 00:38

Fix the using and the number being put on separate lines

ff707b1

Fix merge

6f98e11

Disable the "Try this:" message

4e4a807

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 23, 2026

mathlib-triage Bot assigned JovanGerb May 23, 2026

grunweg reviewed May 23, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/LSeries/HurwitzZeta.lean Outdated

Line length

5230f24

mathlib-bors Bot changed the title ~~feat(Tactic): automatically replace convert with convert!~~ [Merged by Bors] - feat(Tactic): automatically replace convert with convert! May 23, 2026

mathlib-bors Bot closed this May 23, 2026

Uh oh!

Conversation

Vierkantor commented May 22, 2026 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 5230f2468c

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

grunweg commented May 22, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 22, 2026

Uh oh!

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

Uh oh!

Commit Verification Summary

Commits to Review (15)

❌ Automated commits (2) — 0/2 verified

Uh oh!

grunweg commented May 23, 2026

Uh oh!

mathlib-bors Bot commented May 23, 2026

Uh oh!

Uh oh!

grunweg commented May 23, 2026

Uh oh!

grunweg commented May 23, 2026

Uh oh!

mathlib-bors Bot commented May 23, 2026

Uh oh!

grunweg commented May 23, 2026

Uh oh!

mathlib-bors Bot commented May 23, 2026

Uh oh!

grunweg commented May 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Vierkantor commented May 22, 2026 •

edited by grunweg

Loading

github-actions Bot commented May 22, 2026 •

edited

Loading

github-actions Bot commented May 22, 2026 •

edited

Loading