no goals
α : Type u_1
β : Type u_2
γ : Type ?u.45713
δ : Type ?u.45716
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
hs_nonempty : Set.Nonempty s
hs_ne_univ : s ≠ univ
x y : β
⊢ SimpleFunc.range (piecewise s hs (const α x) (const α y)) = {x, y}
simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const,
  Finset.coe_insert, Finset.coe_singleton, hs_nonempty.image_const,
  (nonempty_compl.2 hs_ne_univ).image_const, singleton_union, Function.const]