rintro ⟨a, rfl⟩
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
h : ∀ (m : ℕ), ↑m < n
⊢ ¬∃ a, ↑a = n
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
a : ℕ
h : ∀ (m : ℕ), ↑m < ↑a
⊢ False