Product of finite element in commutative ring

Stream: general

[UHU]

I've got a finite set S

S: Set α
f: Finite ↑S

and a commutative ring R with one of its ideal I

R: Type u
inst✝: CommRing R
I: Ideal R

Furthermore, assume that for each element in S, there exists some element in I that satisfy some property (called P)

h: ∀ i ∈ S, ∃ r ∈ I,  P r

I want to pick an arbitrary element (r i∈I) for each i∈S, and compute their product (which is well-defined since the set S is finite, and the result does not depend on the order since the ring is commutative).
How should I achieve this?

[Eric Wieser]

Does choose r hr pr using h help?

[Kyle Miller]

You should be able to do have := Fintype.ofFinite S and then you get S.toFinset, which might be a little annoying to work with since it's a Finset α and your condition has the dependence on being an element of S, and (Finset.univ : Finset S), which gives you elements of S and might be easier to work with. Then there's docs#Finset.prod