Commit 2025-12-11 07:09 3128d20e
View on Github →feat: add @[grind inj] to Finset.coe_injective (#32714)
Requested at [#lean4 > `grind` doesn't use the fact that Prop is a Subsingleton @ 💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60grind.60.20doesn't.20use.20the.20fact.20that.20Prop.20is.20a.20Subsingleton/near/555663373), seems reasonable.