case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (restrict (range f) (extend f g g'))

case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (restrict (range fᶜ) (extend f g g'))
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')
refine' measurable_of_restrict_of_restrict_compl hf.measurableSet_range _ _
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x => g (Exists.choose (_ : ↑x ∈ range f))
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (restrict (range f) (extend f g g'))
rw [restrict_extend_range]
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x => g (Exists.choose (_ : ↑x ∈ range f))
simpa only [rangeSplitting] using hg.comp hf.measurable_rangeSplitting
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (restrict (range fᶜ) (extend f g g'))
rw [restrict_extend_compl_range]
no goals
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.381496
δ' : Type ?u.381499
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)
exact hg'.comp measurable_subtype_coe