ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
let s : Set α := toMeasurable μ ({ x | f x = H.mk f x ∧ f x ∈ t }ᶜ)
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
case refine'_1
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ Measurable g

case refine'_2
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ range g ⊆ t

case refine'_3
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ f =ᶠ[ae μ] g
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
refine' ⟨g, _, _, _⟩
no goals
case refine'_1
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ Measurable g
exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
case refine'_2.intro
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
⊢ g x ∈ t
case refine'_2
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ range g ⊆ t
rintro _ ⟨x, rfl⟩
case pos
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t

case neg
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬x ∈ s
⊢ g x ∈ t
case refine'_2.intro
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
⊢ g x ∈ t
by_cases hx : x ∈ s
no goals
case pos
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t
simpa [hx] using h₀.some_mem
case neg
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬x ∈ s
⊢ mk f H x ∈ t
case neg
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬x ∈ s
⊢ g x ∈ t
simp only [hx, piecewise_eq_of_not_mem, not_false_iff]
case neg
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬mk f H x ∈ t
⊢ x ∈ toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
case neg
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬x ∈ s
⊢ mk f H x ∈ t
contrapose! hx
case neg.a
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬mk f H x ∈ t
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
case neg
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬mk f H x ∈ t
⊢ x ∈ toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
apply subset_toMeasurable
no goals
case neg.a
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬mk f H x ∈ t
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
simp (config := { contextual := true }) only [hx, mem_compl_iff, mem_setOf_eq, not_and,
  not_false_iff, imp_true_iff]
case refine'_3
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) = 0
⊢ f =ᶠ[ae μ] g
case refine'_3
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ f =ᶠ[ae μ] g
have A : μ (toMeasurable μ ({ x | f x = H.mk f x ∧ f x ∈ t }ᶜ)) = 0 := by
  rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
  exact H.ae_eq_mk.and ht
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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 = piecewise (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) (fun x => Set.Nonempty.some h₀) (mk f H) x
case refine'_3
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) = 0
⊢ f =ᶠ[ae μ] g
filter_upwards [compl_mem_ae_iff.2 A]with x hx
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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 = piecewise (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) (fun x => Set.Nonempty.some h₀) (mk f H) x
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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 = piecewise (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) (fun x => Set.Nonempty.some h₀) (mk f H) x
rw [mem_compl_iff] at hx
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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 = mk f H x
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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 = piecewise (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) (fun x => Set.Nonempty.some h₀) (mk f H) x
simp only [hx, piecewise_eq_of_not_mem, not_false_iff]
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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}ᶜ)
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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 = mk f H x
contrapose! hx
case h.a
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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}ᶜ
case h
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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}ᶜ)
apply subset_toMeasurable
no goals
case h.a
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (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}ᶜ
simp only [hx, mem_compl_iff, mem_setOf_eq, false_and_iff, not_false_iff]
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ {x | f x = mk f H x ∧ f x ∈ t} ∈ ae μ
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ ↑↑μ (toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)) = 0
rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
no goals
ι : Type ?u.2621215
α : Type u_1
β : Type u_2
γ : Type ?u.2621224
δ : Type ?u.2621227
R : Type ?u.2621230
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ ({x | f x = mk f H x ∧ f x ∈ t}ᶜ)
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ {x | f x = mk f H x ∧ f x ∈ t} ∈ ae μ
exact H.ae_eq_mk.and ht