no goals
α : Type u_1
β : Type u_2
γ : Type ?u.12684
δ : Type ?u.12687
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y, y ∈ SimpleFunc.range f ∧ p y) ↔ ∃ x, p (↑f x)
simpa only [mem_range, exists_prop] using Set.exists_range_iff