no goals
α : Type u_1
β : Type u_2
γ : Type ?u.381096
δ : Type ?u.381099
δ' : Type ?u.381102
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)
rwa [preimage_rangeSplitting hf.injective,
  ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
  coe_comp_rangeFactorization, hf.measurableSet_image]