no goals
α : Type u_1
β : Type u_2
γ : Type ?u.376105
δ : Type ?u.376108
δ' : Type ?u.376111
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
⊢ MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s
simp [measurableSet_sum_iff, Sum.inl_injective.preimage_image]