no goals
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.57313
inst✝¹ : MeasurableSpace α
inst✝ : DecidableEq γ
g : β → γ
f : α →ₛ β
⊢ ↑(SimpleFunc.range (map g f)) = ↑(Finset.image g (SimpleFunc.range f))
simp only [coe_range, coe_map, Finset.coe_image, range_comp]