Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(ring_theory/ideal/basic): ideal.module_pi speedup (#9148)
Eric and Yael were both complaining that `ideal.module_pi` would occasionally cause random timeouts on unrelated PRs. This PR (a) makes the `smul` proof obligation much tidier (factoring out a sublemma) and (b) replaces the `all_goals` trick by 6 slightly more refined proofs (making the new proof longer, but quicker). On my machine the profiler stats are: ``` ORIG parsing took 74.1ms elaboration of module_pi took 3.83s type checking of module_pi took 424ms decl post-processing of module_pi took 402ms NEW parsing took 136ms elaboration of module_pi took 1.19s type checking of module_pi took 82.8ms decl post-processing of module_pi took 82.5ms ```
- Loading branch information
Showing
1 changed file
with
42 additions
and
19 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters