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] - feat(*): several @[simp]
lemmas
#2579
Conversation
Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`.
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.
LGTM
bors merge
@@ -584,6 +584,14 @@ by simp [and_comm] | |||
@[simp] theorem exists_eq_right {a' : α} : (∃ a, p a ∧ a = a') ↔ p a' := | |||
(exists_congr $ by exact λ a, and.comm).trans exists_eq_left | |||
|
|||
@[simp] theorem exists_exists_and_eq_and {f : α → β} {p : α → Prop} {q : β → Prop} : |
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.
I can imagine that there are 37 permutations of these lemmas, but maybe these two are the only ones that typically show up in a "simp-path"...
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.
These two come from ∃ y ∈ f '' s
and ∃ y ∈ set.range f
.
Build failed: |
bors r- |
Build fails because of mid-proof |
| left := ↑(λ n : ℕ, n.unpair.1) | ||
| right := ↑(λ n : ℕ, n.unpair.2) |
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.
There's a very similar timeout issue here: https://github.com/leanprover-community/mathlib/blob/master/src/computability/partrec.lean#L149
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.
Do you have an idea why this became an issue after #2363? It was ~1s before and ~70s after.
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.
Unfortunately, no. Have you looked at type class search traces before and after?
bors r+ |
Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by #2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code
Pull request successfully merged into master. Build succeeded: |
@[simp]
lemmas@[simp]
lemmas
Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by leanprover-community#2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code
Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by leanprover-community#2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code
Also add an explicit instance for `submodule.has_coe_to_sort`. This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`. Also fixes some timeouts introduced by leanprover-community#2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code
Also add an explicit instance for
submodule.has_coe_to_sort
.This way
rintro ⟨x, hx⟩
results in(hx : x ∈ p)
.Also fixes some timeouts introduced by #2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code