rintro ⟨n, hn⟩
Q : ℕ → Prop
inst✝ : DecidablePred Q
⊢ (∃ n, ∀ (k : ℕ), Q k → k ≤ n) → ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s
case intro
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s