`SampleableType (α × β)` instance carries unneeded `[Fintype]`/`[Inhabited]` constraints

[astefano]

The product instance requires [Fintype α] [Fintype β] [Inhabited α] [Inhabited β], but they don't seem to be needed anymore:

• Fintype only fed the original cardinality-based probOutput_selectElem_eq proof (via probOutput_uniformSample, [Fintype]). A Fintype-free proof exists using probOutput_seq_map_prod_mk_eq_mul + the class's own probOutput_selectElem_eq per component.
• Inhabited fed the old probFailure_selectElem field, deleted in chore: update to 4.27 #97.

The class itself doesn't seem to need Fintype (its docstring seems to say so). The constraints just block
SampleableType (α × β) for abstract SampleableType carriers with no Fintype.

We could relax to [SampleableType α] [SampleableType β] only (same selectElem), and optionally add uniformSample_prod_eq_bind : $ᵗ(α×β) = do a ← $ᵗα; b ← $ᵗβ; pure (a,b).

The cost is that PRGfromPRF.lean declares [Fintype S/O] [Inhabited S/O] as section vars used only to synthesize SampleableType (S × O); relaxing makes them unused on some decls, tripping the unused-Fintype linter. So it needs a targeted signature cleanup there (~20 hyps, some public).

Would a PR dropping the constraints be of interest?

[dtumad]

Solved in #459