no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.60622
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β →ₛ γ
g : α → β
hgm : Measurable g
⊢ ↑(SimpleFunc.range (comp f g hgm)) ⊆ ↑(SimpleFunc.range f)
simp only [coe_range, coe_comp, Set.range_comp_subset_range]