apply Nat.lt_succ_of_le
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < s.sup id + 1
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ s.sup id