case intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
ι : Type ?u.343332
inst✝³ : MeasurableSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
α : Type u_1
inst✝⁴ : TopologicalSpace α
ι : Type ?u.343332
inst✝³ : MeasurableSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
inst✝ : Finite α
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α
case intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
ι : Type ?u.343332
inst✝³ : MeasurableSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ ↑(range fun x => ↑↑x)
case intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
ι : Type ?u.343332
inst✝³ : MeasurableSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
refine' ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans _)⟩⟩
no goals
case intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
ι : Type ?u.343332
inst✝³ : MeasurableSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ ↑(range fun x => ↑↑x)
exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)