-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem subtype_mk (h : AEMeasurable f μ) {s : Set β} {hfs : ∀ x, f x ∈ s} :
    AEMeasurable (codRestrict f s hfs) μ

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : 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

Tactic:
simpa [Subtype.ext_iff]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
refine ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : 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 ⋯

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : 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 ⋯

Tactic:
filter_upwards [fg] with x hx

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : 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

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
nontriviality α

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs) μ

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
inhabit α

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs) μ

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
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⟩

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ AEMeasurable (codRestrict f s hfs) μ