[Merged by Bors] - chore(group_theory/perm/sign): remove classical for sign congr simp lemmas #5622
Conversation
pechersky
added
the
awaiting-review
| rw [← finset.univ_product_univ, finset.prod_product, finset.prod_comm], | ||
| simp }, | ||
| rw [finset.prod_mul_distrib, ←finset.univ_product_univ, finset.prod_product, finset.prod_comm], | ||
| simp [sign_prod_congr_left] }, |
There was a problem hiding this comment.
This is a great improvement!
I wasn't aware that using classical like this could be an issue. Are there other places where this pops up?
There was a problem hiding this comment.
Yes, the sign lemmas simplifying various congr were causing me a lot of pain trying to simplify pretty obvious equiv_congr.map_equiv option, because the decidable_eq instance for option α is easily constructed from the [decidable_eq α], but the relevant lemma had no explicit decidable_eq! I was so confused, until I noticed the open_locale classical that was near the end of the file. Some new sign lemmas didn't have this issue because they used different Type arguments.
There was a problem hiding this comment.
I found an earlier Zulip thread that discussed a similar issue and mentioned this PR on Zulip.
github-actions
bot
added
ready-to-merge
…emmas (#5622) Previously, some lemmas about how `perm.sign` simplifies across various congrs of permutations assumed `classical`, which prevented them from being applied by the simplifier. This makes the `decidable_eq` assumptions explicit.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Previously, some lemmas about how
perm.signsimplifies across various congrs of permutations assumedclassical, which prevented them from being applied by the simplifier. This makes thedecidable_eqassumptions explicit.