-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.ContinuousOn.measurableEmbedding [BorelSpace β]
    [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ]
    (hs : MeasurableSet s) (f_cont : ContinuousOn f s)
    (f_inj : InjOn f s) : MeasurableEmbedding (s.restrict f) :=
  { injective := injOn_iff_injective.1 f_inj
    measurable := (continuousOn_iff_continuous_restrict.1 f_cont).measurable
    measurableSet_image'

Proof state:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ ∀ ⦃s_1 : Set ↑s⦄, MeasurableSet s_1 → MeasurableSet (s.restrict f '' s_1)

Tactic:
intro u hu

Result:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
⊢ MeasurableSet (s.restrict f '' u)

Proof state:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
A : MeasurableSet (Subtype.val '' u)
⊢ MeasurableSet (s.restrict f '' u)

Tactic:
have B : MeasurableSet (f '' (((↑) : s → γ) '' u)) :=
  A.image_of_continuousOn_injOn (f_cont.mono (Subtype.coe_image_subset s u))
    (f_inj.mono (Subtype.coe_image_subset s u))

Result:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
A : MeasurableSet (Subtype.val '' u)
B : MeasurableSet (f '' (Subtype.val '' u))
⊢ MeasurableSet (s.restrict f '' u)

Proof state:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
A : MeasurableSet (Subtype.val '' u)
B : MeasurableSet (f '' (Subtype.val '' u))
⊢ MeasurableSet (s.restrict f '' u)

Tactic:
rwa [← image_comp] at B

Result:
no goals

Proof state:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
⊢ MeasurableSet (s.restrict f '' u)

Tactic:
have A : MeasurableSet (((↑) : s → γ) '' u) :=
  (MeasurableEmbedding.subtype_coe hs).measurableSet_image.2 hu

Result:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
A : MeasurableSet (Subtype.val '' u)
⊢ MeasurableSet (s.restrict f '' u)