[Merged by Bors] - feat(push): push annotations for Real.log#30039
[Merged by Bors] - feat(push): push annotations for Real.log#30039JovanGerb wants to merge 10 commits intoleanprover-community:masterfrom
push annotations for Real.log#30039Conversation
PR summary ee728d5a73Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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
|
|
This pull request has conflicts, please merge |
| rw [← prod_map_toList, log_list_prod (by simp_all)] | ||
| simp | ||
|
|
||
| @[push] |
There was a problem hiding this comment.
This side condition seems somewhat non-trivial to discharge --- so currently, this lemma will not always apply. That said, there's not much harm in having it anyway, you can probably use a discharger to prove it in practice (and we will hopefully have support for discharging side goals properly).
There was a problem hiding this comment.
Yes, we would like to have push create side goals, so that this side goal can be shown to the user.
| example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : Real.log (a * b) = Real.log a + Real.log b := by | ||
| pull (disch := positivity) Real.log | ||
| rfl | ||
|
|
There was a problem hiding this comment.
Can you also add a test for some of the other lemmas, and a test for the rpow bug?
@[push] annotations for Real.logpush annotations for Real.log
grunweg
left a comment
There was a problem hiding this comment.
Thanks! Looks good to me, with comments addressed. Please also mention the reason for allowing a term head in the PR description; that's really useful context!
|
LGTM with master merged and a test for |
|
✌️ JovanGerb can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
This PR adds `push` annotations, and tests for `Real.log`. It also updates the `#push` and `#pull` commands so that they can take a discharger, and can take any head.
|
Pull request successfully merged into master. Build succeeded: |
push annotations for Real.logpush annotations for Real.log
This PR adds
pushannotations, and tests forReal.log.It also updates the
#pushand#pullcommands so that they can take a discharger, and can take any head.