-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/multivariate/qpf): definition #3395
Conversation
0660864
to
10ea41b
Compare
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
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've marked a few nonterminal simp
calls.
@avigad to approve a PR you now have to leave a comment with bors merge
on a new line, rather than adding the green label. The label will get added automatically when you comment.
ext, simp [supp], split; intro h, | ||
{ apply @h (λ i x, ∃ (y : P.B a i), f i y = x), | ||
rw liftp_iff', intros, refine ⟨_,rfl⟩ }, | ||
{ simp [liftp_iff'], cases h, subst x, |
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.
nonterminal simp
s
src/data/qpf/multivariate/basic.lean
Outdated
simp [liftp_iff_of_is_uniform,supp_eq_of_is_uniform,mvpfunctor.liftp_iff',h'], | ||
split; intros; subst_vars; solve_by_elim }, | ||
{ rintros α ⟨a,f⟩, | ||
simp [liftp_preservation] at h, |
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.
nonterminal simp
s
@robertylewis Thanks for the extra check (and information). Are the nonterminal |
@avigad I believe the recommended style is for |
I think this might be a good reference: https://leanprover-community.github.io/extras/simp.html#when-it-is-unadvisable-to-use-simp |
Yes, that looks right. |
Trusting Jeremy's approval when I write bors merge |
👎 Rejected by label |
and again, bors merge |
Pull request successfully merged into master. Build succeeded: |
Part of #3317