no goals
α : Type ?u.3040955
β : Type ?u.3040958
γ : Type ?u.3040961
γ₂ : Type ?u.3040964
δ : Type ?u.3040967
ι : Sort y
s t u : Set α
inst✝ : MeasurableSpace α
⊢ Measurable fun p => EReal.toReal ↑p
simpa using measurable_id