[Merged by Bors] - chore(Imo/Imo1964Q1): minor clean-up#19691
[Merged by Bors] - chore(Imo/Imo1964Q1): minor clean-up#19691
Conversation
PR summary 1d8fd85c77Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
grunweg
left a comment
There was a problem hiding this comment.
Generally looks good, thanks! I'd like one sentence to be changed (which is easy), and would like maintainer sign-off on a policy question (see inline comment).
maintainer delegate?
| /-! | ||
| ## The question | ||
| -/ | ||
| _ = 2 ^ t := by rw [one_pow, one_mul] |
There was a problem hiding this comment.
As I understand it, the archive's purpose is also about showcasing idiomatic Lean's abilities. Using ring seems in line with that; I'm sceptical about un-automating it in general. (There was a zulip thread about using automation in mathlib, a few months ago. I could try to dig it up.)
In this case (reducing imports significantly, for one line which becomes slightly longer), I'm fine with accepting this.
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
This PR does the following: - remove some trivial sectioning - explain the solution better - remove `ProblemPredicate`, which was only used once - replace `ring` by a short `rw` (to minimize imports)
|
Pull request successfully merged into master. Build succeeded: |
This reverts a change from #19691, which unnecessarily removed a tactic invocation in favour of writing out lemmas. The archive should be demonstrating good style, and unless there is a verbosity or speed issue, robust and well specified tactics should always be preferred over proofs that require knowing lemmas (even if, as in this case, those lemmas are easy to identify and use).
This PR does the following:
ProblemPredicate, which was only used onceringby a shortrw(to minimize imports)