use s.sup id + 1
case intro
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∃ n, ∀ (k : ℕ), Q k → k < n
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < s.sup id + 1