case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.401587
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
s : Set ℝ
hs : MeasurableSet s
e : α ≃ᵐ ↑s
⊢ ∃ f, MeasurableEmbedding f
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.401587
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
⊢ ∃ f, MeasurableEmbedding f
obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α
no goals
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.401587
inst✝² : MeasurableSpace α
inst✝¹ : PolishSpace α
inst✝ : BorelSpace α
s : Set ℝ
hs : MeasurableSet s
e : α ≃ᵐ ↑s
⊢ ∃ f, MeasurableEmbedding f
exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩