no goals
α : Type u_2
β : Type u_1
γ : Type ?u.377196
δ : Type ?u.377199
δ' : Type ?u.377202
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
⊢ MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
simp [measurableSet_sum_iff, Sum.inr_injective.preimage_image]