ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs)
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ AEMeasurable (codRestrict f s hfs)
nontriviality α
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs)
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs)
inhabit α
case intro.intro.intro
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ AEMeasurable (codRestrict f s hfs)
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs)
obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
  h.exists_ae_eq_range_subset (eventually_of_forall hfs) ⟨_, hfs default⟩
case intro.intro.intro
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ codRestrict f s hfs =ᶠ[ae μ] codRestrict g s (_ : ∀ (x : α), g x ∈ s)
case intro.intro.intro
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ AEMeasurable (codRestrict f s hfs)
refine' ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, _⟩
case h
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ codRestrict f s hfs x = codRestrict g s (_ : ∀ (x : α), g x ∈ s) x
case intro.intro.intro
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ codRestrict f s hfs =ᶠ[ae μ] codRestrict g s (_ : ∀ (x : α), g x ∈ s)
filter_upwards [fg] with x hx
no goals
case h
ι : Type ?u.2834714
α : Type u_1
β : Type u_2
γ : Type ?u.2834723
δ : Type ?u.2834726
R : Type ?u.2834729
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ codRestrict f s hfs x = codRestrict g s (_ : ∀ (x : α), g x ∈ s) x
simpa [Subtype.ext_iff]