no goals
α : Type u_1
β : Type u_2
γ : Type ?u.380860
δ : Type ?u.380863
δ' : Type ?u.380866
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
rw [← image_preimage_eq_inter_range, hf.measurableSet_image]