∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : MeasurableSpace Z]
  [MeasurableSpace.CountablySeparated Z] {f : X → Z},
  Measurable f → Function.Surjective f → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s