-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
/-- Let `f : α → β` be a null measurable function
such that a.e. all values of `f` belong to a set `t`
such that the restriction of the `σ`-algebra in the codomain to `t` is countably generated,
then `f` is a.e.-measurable. -/
lemma MeasureTheory.NullMeasurable.aemeasurable_of_aerange {f : α → β} {t : Set β}
    [MeasurableSpace.CountablyGenerated t] (h : NullMeasurable f μ) (hft : ∀ᵐ x ∂μ, f x ∈ t) :
    AEMeasurable f μ

Proof state:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ

Tactic:
obtain ⟨f', hf'm, hf't, hff'⟩ :
    ∃ f' : α → β, NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᵐ[μ] f' :=
  h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : range f' ⊆ t
hff' : f =ᶠ[ae μ] f'
⊢ AEMeasurable f μ

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : range f' ⊆ t
hff' : f =ᶠ[ae μ] f'
⊢ AEMeasurable f μ

Tactic:
rw [range_subset_iff] at hf't

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : ∀ (y : α), f' y ∈ t
hff' : f =ᶠ[ae μ] f'
⊢ AEMeasurable f μ

Proof state:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ

Tactic:
rw [← μ.ae_completion] at hft

Result:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ

Proof state:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
h : NullMeasurable f 0
hft : ∀ᵐ (x : α) ∂0, f x ∈ ∅
⊢ AEMeasurable f 0

Tactic:
apply aemeasurable_zero_measure

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable f μ

Tactic:
rcases eq_empty_or_nonempty t with rfl | hne

Result:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ AEMeasurable f μ

case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : ∀ (y : α), f' y ∈ t
hff' : f =ᶠ[ae μ] f'
⊢ AEMeasurable f μ

Tactic:
lift f' to α → t using hf't

Result:
case inr.intro.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → ↑t
hf'm : NullMeasurable (fun i => ↑(f' i)) μ
hff' : f =ᶠ[ae μ] fun i => ↑(f' i)
⊢ AEMeasurable f μ

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ μ = 0

Tactic:
simpa using hft

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → ↑t
hff' : f =ᶠ[ae μ] fun i => ↑(f' i)
hf'm : NullMeasurable f' μ
⊢ AEMeasurable f μ

Tactic:
exact (measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ AEMeasurable f μ

Tactic:
obtain rfl : μ = 0 := by simpa using hft

Result:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
h : NullMeasurable f 0
hft : ∀ᵐ (x : α) ∂0, f x ∈ ∅
⊢ AEMeasurable f 0

Proof state:
case inr.intro.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → ↑t
hf'm : NullMeasurable (fun i => ↑(f' i)) μ
hff' : f =ᶠ[ae μ] fun i => ↑(f' i)
⊢ AEMeasurable f μ

Tactic:
replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk

Result:
case inr.intro.intro.intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → ↑t
hff' : f =ᶠ[ae μ] fun i => ↑(f' i)
hf'm : NullMeasurable f' μ
⊢ AEMeasurable f μ