∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : α → β) (h : ∀ (x : β), MeasurableSet (f ⁻¹' {x}))
  (h' : (Set.range f).Finite), ⇑{ toFun := f, measurableSet_fiber' := h, finite_range' := h' } = f