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.

Author: kim-em

Mathlib/Data/Finset/Defs.lean

@@ -159,6 +159,7 @@ theorem ext {s₁ s₂ : Finset α} (h : ∀ a, a ∈ s₁ ↔ a ∈ s₂) : s
 theorem coe_inj {s₁ s₂ : Finset α} : (s₁ : Set α) = s₂ ↔ s₁ = s₂ :=
   SetLike.coe_set_eq
 
+@[grind inj]
 theorem coe_injective {α} : Injective ((↑) : Finset α → Set α) := fun _s _t => coe_inj.1
 
 /-! ### type coercion -/