simp_rw [eq_comm (a := s), image_preimage_eq_iff, range_coe', Iio, lt_top_iff_ne_top,
  ← compl_singleton_eq, subset_compl_singleton_iff]
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ s = Nat.cast '' (Nat.cast ⁻¹' s)
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
s : Set ℕ∞
h : ⊤ ∉ s
⊢ ⊤ ∉ s