-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.image_of_measurable_injOn {f : γ → α}
    [MeasurableSpace.CountablySeparated α]
    [MeasurableSpace γ] [StandardBorelSpace γ]
    (hs : MeasurableSet s) (f_meas : Measurable f) (f_inj : InjOn f s) :
    MeasurableSet (f '' s)

Proof state:
case intro.intro.intro
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
⊢ MeasurableSet (f '' s)

Tactic:
obtain ⟨t', t't, f_cont, t'_polish⟩ :
    ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' :=
  f_meas.exists_continuous

Result:
case intro.intro.intro.intro.intro.intro
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
⊢ MeasurableSet (f '' s)

Proof state:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
letI := upgradeStandardBorel γ

Result:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
⊢ MeasurableSet (f '' s)

Proof state:
case intro.intro.intro.intro.intro.intro
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
M : MeasurableSet s
⊢ MeasurableSet (f '' s)

Tactic:
exact
  @MeasurableSet.image_of_continuousOn_injOn γ
    _ _ _ _  s f _ t' t'_polish (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)
    M (@Continuous.continuousOn γ _ t' _ f s f_cont) f_inj

Result:
no goals

Proof state:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
⊢ MeasurableSet (f '' s)

Tactic:
let tγ : TopologicalSpace γ := inferInstance

Result:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
⊢ MeasurableSet (f '' s)

Proof state:
case intro.intro.intro.intro.intro.intro
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
⊢ MeasurableSet (f '' s)

Tactic:
have M : MeasurableSet[@borel γ t'] s :=
  @Continuous.measurable γ γ t' (@borel γ t')
    (@BorelSpace.opensMeasurable γ t' (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl))
    tγ _ _ _ (continuous_id_of_le t't) s hs

Result:
case intro.intro.intro.intro.intro.intro
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
M : MeasurableSet s
⊢ MeasurableSet (f '' s)

Proof state:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
⊢ MeasurableSet (f '' s)

Tactic:
rcases exists_opensMeasurableSpace_of_countablySeparated α with ⟨τ, _, _, _⟩

Result:
case intro.intro.intro
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
⊢ MeasurableSet (f '' s)