no goals
α : Type u_1
β : Type u_2
γ : Type ?u.379194
δ : Type ?u.379197
δ' : Type ?u.379200
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
s : Set α
h : MeasurableSet (f '' s)
⊢ MeasurableSet s
simpa only [hf.injective.preimage_image] using hf.measurable h