Zulip Chat Archive
Stream: mathlib4
Topic: simps for MulOpposite
Yury G. Kudryashov (Jun 20 2023 at 02:36):
I've noticed that docs4#MulOpposite.opHomeomorph has wrong simp lemmas generated by simps (compare with docs#mul_opposite.op_homeomorph).
Yury G. Kudryashov (Jun 20 2023 at 02:37):
First, it generates apply_unop' instead of apply. Second, it uses unop' instead of unop.
Yury G. Kudryashov (Jun 20 2023 at 02:56):
I can try to fix it tomorrow (in this and other files).
Eric Wieser (Jun 20 2023 at 07:03):
The first one is fallout from making it a structure
Eric Wieser (Jun 20 2023 at 07:04):
The second one is annoying to fix; I don't think simps allows custom projections on type synonyms, though it should.
Floris van Doorn (Jun 20 2023 at 13:22):
If you don't want to recurse into MulOpposite/AddOpposite, you can add PreOpposite to https://github.com/leanprover-community/mathlib4/blob/6533094a68393dbab56cfb3ff2bed55c6978a84d/Mathlib/Tactic/Simps/Basic.lean#L837
And indeed, simps doesn't (currently) allow custom projections for type synonyms.
Yury G. Kudryashov (Jun 23 2023 at 20:08):
#5434 (awaiting CI)
Last updated: Dec 20 2023 at 11:08 UTC