-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem exists_ae_eq_range_subset (H : AEMeasurable f μ) {t : Set β} (ht : ∀ᵐ x ∂μ, f x ∈ t)
    (h₀ : t.Nonempty) : ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g

Proof state:
case pos
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t

Tactic:
simpa [g, hx] using h₀.some_mem

Result:
no goals

Proof state:
case h.a
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ

Tactic:
simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
x : α
⊢ g x ∈ t

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t

case neg
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
x : α
hx : x ∉ s
⊢ g x ∈ t

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Tactic:
let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ

Tactic:
apply subset_toMeasurable

Result:
case h.a
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : x ∈ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ)ᶜ
⊢ f x = g x

Tactic:
rw [mem_compl_iff] at hx

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
A : μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : x ∉ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = g x

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Tactic:
refine ⟨g, ?_, ?_, ?_⟩

Result:
case refine_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ Measurable g

case refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ range g ⊆ t

case refine_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ f =ᶠ[ae μ] g

Proof state:
case neg
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
x : α
hx : mk f H x ∉ t
⊢ x ∈ s

Tactic:
apply subset_toMeasurable

Result:
case neg.a
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
x : α
hx : mk f H x ∉ t
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0

Tactic:
rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ {x | f x = mk f H x ∧ f x ∈ t} ∈ ae μ