α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))
α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))
have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
  Nat.closedEmbedding_coe_real.isClosedMap.closed_range.polishSpace
α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ α ≃ ↑(range Nat.cast)
α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))
refine' ⟨PolishSpace.Equiv.measurableEquiv _⟩
α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ ℕ ≃ ↑(range Nat.cast)
α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ α ≃ ↑(range Nat.cast)
refine' (nonempty_equiv_of_countable.some : α ≃ ℕ).trans _
no goals
α : Type u_1
inst✝⁵ : TopologicalSpace α
ι : Type ?u.398049
inst✝⁴ : MeasurableSpace α
inst✝³ : PolishSpace α
inst✝² : BorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ ℕ ≃ ↑(range Nat.cast)
exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective