-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable;
a version for the region together with the graphs of both functions. -/
lemma nullMeasurableSet_region_between_cc (μ : Measure α)
    {f g : α → ℝ} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ)
    {s : Set α} (s_mble : NullMeasurableSet s μ) :
    NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.snd ∈ Icc (f p.fst) (g p.fst)} (μ.prod volume)

Proof state:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => p.2 ≤ g p.1) (μ.prod volume)

Tactic:
change NullMeasurableSet {p : α × ℝ | p.snd ≤ g p.fst} (μ.prod volume)

Result:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.2 ≤ g p.1} (μ.prod volume)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ {p | f p.1 ≤ p.2} = {p | p.2 < f p.1}ᶜ

Tactic:
ext p

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
p : α × ℝ
⊢ p ∈ {p | f p.1 ≤ p.2} ↔ p ∈ {p | p.2 < f p.1}ᶜ

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ {p | p.2 ≤ g p.1} = {p | g p.1 < p.2}ᶜ

Tactic:
ext p

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
p : α × ℝ
⊢ p ∈ {p | p.2 ≤ g p.1} ↔ p ∈ {p | g p.1 < p.2}ᶜ

Proof state:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.2 ≤ g p.1} (μ.prod volume)

Tactic:
rw [show {p : α × ℝ | p.snd ≤ g p.fst} = {p : α × ℝ | g p.fst < p.snd}ᶜ by
      ext p
      simp only [mem_setOf_eq, mem_compl_iff, not_lt]]

Result:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | g p.1 < p.2}ᶜ (μ.prod volume)

Proof state:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | g p.1 < p.2}ᶜ (μ.prod volume)

Tactic:
exact (nullMeasurableSet_lt (AEMeasurable.fst g_mble) measurable_snd.aemeasurable).compl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => f p.1 ≤ p.2) (μ.prod volume)

Tactic:
change NullMeasurableSet {p : α × ℝ | f p.fst ≤ p.snd} (μ.prod volume)

Result:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | f p.1 ≤ p.2} (μ.prod volume)

Proof state:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.2 < f p.1}ᶜ (μ.prod volume)

Tactic:
exact (nullMeasurableSet_lt measurable_snd.aemeasurable (AEMeasurable.fst f_mble)).compl

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
p : α × ℝ
⊢ p ∈ {p | p.2 ≤ g p.1} ↔ p ∈ {p | g p.1 < p.2}ᶜ

Tactic:
simp only [mem_setOf_eq, mem_compl_iff, not_lt]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)} (μ.prod volume)

Tactic:
refine NullMeasurableSet.inter
        (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)

Result:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => f p.1 ≤ p.2) (μ.prod volume)

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => p.2 ≤ g p.1) (μ.prod volume)

Proof state:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | f p.1 ≤ p.2} (μ.prod volume)

Tactic:
rw [show {p : α × ℝ | f p.fst ≤ p.snd} = {p : α × ℝ | p.snd < f p.fst}ᶜ by
      ext p
      simp only [mem_setOf_eq, mem_compl_iff, not_lt]]

Result:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.2 < f p.1}ᶜ (μ.prod volume)

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
p : α × ℝ
⊢ p ∈ {p | f p.1 ≤ p.2} ↔ p ∈ {p | p.2 < f p.1}ᶜ

Tactic:
simp only [mem_setOf_eq, mem_compl_iff, not_lt]

Result:
no goals