no goals
α : Type ?u.71312
β : Type ?u.71315
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s
rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]