Zulip Chat Archive
Stream: mathlib4
Topic: simp failure in !4#2390
Yury G. Kudryashov (Feb 20 2023 at 08:52):
In !4#2390, simp fails to simplify FunLike.coe (Finset.mapEmbedding f) a to Finset.map f a. I have no idea why.
Last updated: May 02 2025 at 03:31 UTC