α β : Type u
n : ℕ
⊢ ↑(choose (_ : ∃ n_1, ↑n = ↑n_1)) = ↑n
α β : Type u
n : ℕ
⊢ ↑toNat ↑n = n
rw [toNat_apply_of_lt_aleph0 (nat_lt_aleph0 n), ← natCast_inj]
no goals
α β : Type u
n : ℕ
⊢ ↑(choose (_ : ∃ n_1, ↑n = ↑n_1)) = ↑n
exact (Classical.choose_spec (lt_aleph0.1 (nat_lt_aleph0 n))).symm