-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
/-- If the `σ`-algebra of the codomain of a null measurable function is countably generated,
then the function is a.e.-measurable. -/
lemma MeasureTheory.NullMeasurable.aemeasurable {f : α → β}
    [hc : MeasurableSpace.CountablyGenerated β] (h : NullMeasurable f μ) : AEMeasurable f μ

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq

Result:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
⊢ AEMeasurable f μ

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
a✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ AEMeasurable f μ

Tactic:
rcases hc.1 with ⟨S, hSc, rfl⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ

Proof state:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
⊢ Measurable (f ∘ Subtype.val)

Tactic:
refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_

Result:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
s : Set β
hs : s ∈ S
⊢ MeasurableSet (Subtype.val '' (f ∘ Subtype.val ⁻¹' s))

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
⊢ AEMeasurable f μ

Tactic:
choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq

Result:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
⊢ AEMeasurable f μ

Proof state:
case h.e'_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
s : Set β
hs : s ∈ S
⊢ f ⁻¹' s ∩ vᶜ = T s \ v

Tactic:
refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩

Result:
case h.e'_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
s : Set β
hs : s ∈ S
x : α
hxv : x ∈ vᶜ
hx : x ∈ f ⁻¹' s
⊢ x ∈ T s

Proof state:
case intro.intro.refine_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
⊢ Measurable (v.restrict fun x => default)

Tactic:
apply measurable_const

Result:
no goals

Proof state:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
⊢ Measurable (vᶜ.restrict (v.piecewise (fun x => default) f))

Tactic:
rw [restrict_piecewise_compl, restrict_eq]

Result:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
⊢ Measurable (f ∘ Subtype.val)