no goals
α : Type u_1
β : Type u_2
γ : Type ?u.12286
δ : Type ?u.12289
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∀ (y : β), y ∈ SimpleFunc.range f → p y) ↔ ∀ (x : α), p (↑f x)
simp only [mem_range, Set.forall_range_iff]