New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*): speedup slow proofs #7148
Conversation
change algebra R (sections_subalgebra F), | ||
have : algebra R (types.limit_cone (F ⋙ forget (Algebra.{v} R))).X | ||
= algebra R (sections_subalgebra F), by refl, | ||
rw this, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wow, it's sad that this speeds things up.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, a lot of things in this PR are really weird. Here, it even changes the algebra structure that is inferred (see the next change in the PR, adding a convert).
bors merge |
Some proofs using heavy `rfl` or heavy `obviously` can be sped up considerably. Done in this PR for some outstanding examples.
Pull request successfully merged into master. Build succeeded: |
@@ -84,7 +84,7 @@ begin | |||
letI : normed_space ℝ F := normed_space.restrict_scalars _ 𝕜 _, | |||
-- Let `fr: p →L[ℝ] ℝ` be the real part of `f`. | |||
let fr := re_clm.comp (f.restrict_scalars ℝ), | |||
have fr_apply : ∀ x, fr x = re (f x) := λ x, rfl, | |||
have fr_apply : ∀ x, fr x = re (f x), by { assume x, refl }, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This one is bizarre
Some proofs using heavy
rfl
or heavyobviously
can be sped up considerably. Done in this PR for some outstanding examples.Cherry-picked from #7084, in which all the original proofs fixed in this PR timed out because of the added complexity to the definition of
monoid
s andadd_monoid
s. I don't know how long #7084 will take to get merged (or if it will ever get merged), but these seem good to have anyway, as shaving a few minutes from every mathlib compilations can only help.