no goals
α : Type u_1
β : Type u_2
γ : Type ?u.903481
δ : Type ?u.903484
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
x : α
⊢ x ∈ support ↑f ↔ x ∈ ⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}
simp only [mem_support, Set.mem_preimage, mem_filter, mem_range_self, true_and_iff, exists_prop,
  mem_iUnion, Set.mem_range, mem_singleton_iff, exists_eq_right']