Prove non-emptiness of several sets

Stream: new members

[Loïc Simon]

Hello, I'm pretty new to Lean and struggling with hypothesis declarations in a theorem.

I'm working with a finset of finset ℕ and I need to extract the minimal element of each (let's say, to sum them).
I know (by construction) that my sets are not empty, but I don't know how to tell that to finset.min':

The code

(sets: finset (finset ℕ))
(x: ℝ)
[...]
(h1: ∀s: finset ℕ, s ∈ sets → finset.nonempty s)
(h2: x = ∑ s in sets, s.min' (h1 s (s ∈ sets)) )

produces

type mismatch at application
  h1 s (s ∈ sets)
term
  s ∈ sets
has type
  Prop : Type
but is expected to have type
  s ∈ sets : Prop

So I don't really know how to express s ∈ sets in this context; if I put it in another hypothesis I'll have the same issue.
I tried different things without success, this is the closer I got (I think).

Thanks!

[Johan Commelin]

@Loïc Simon This is unfortunately not possible with ∑ s in sets, f s, because f will be a total function, defined on all of finset ℕ.
What you can do is

∑ s : {x : finset ℕ // x ∈ sets}, s.1.min' (h1 s s.2)

[Johan Commelin]

That way you are summing a total function over the subtype of stuff ∈ sets, and hence you will have that property ready when you need it.