α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ ↑↑volume (Subtype.val '' univ) = ↑↑volume s

α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ Injective Subtype.val

α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ ∀ (s_1 : Set ↑s), MeasurableSet s_1 → NullMeasurableSet (Subtype.val '' s_1)
α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ ↑↑volume univ = ↑↑volume s
rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]
case e_a
α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ Subtype.val '' univ = s
α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ ↑↑volume (Subtype.val '' univ) = ↑↑volume s
congr
no goals
case e_a
α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ Subtype.val '' univ = s
simp only [image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
no goals
α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ Injective Subtype.val
exact Subtype.coe_injective
no goals
α : Type u_1
β : Type ?u.270811
γ : Type ?u.270814
δ : Type ?u.270817
ι : Type ?u.270820
R : Type ?u.270823
R' : Type ?u.270826
s : Set α
inst✝ : MeasureSpace α
p : α → Prop
hs : NullMeasurableSet s
⊢ ∀ (s_1 : Set ↑s), MeasurableSet s_1 → NullMeasurableSet (Subtype.val '' s_1)
exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hs