-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_regionBetween_eq_lintegral' (hf : Measurable f) (hg : Measurable g)
    (hs : MeasurableSet s) :
    μ.prod volume (regionBetween f g s) = ∫⁻ y in s, ENNReal.ofReal ((g - f) y) ∂μ

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = s.indicator (fun x => ofReal (g x - f x)) x

Tactic:
rw [indicator_apply]

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0

Tactic:
simp only [hx, measure_empty]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [h, lintegral_indicator] <;> simp only [hs, Pi.sub_apply]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

Tactic:
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

Tactic:
simp only [hx, Real.volume_Ioo, sub_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
dsimp only [regionBetween, preimage_setOf_eq]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)

Tactic:
exact measurableSet_regionBetween hf hg hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (fun x => volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x => ofReal (g x - f x)

Tactic:
funext x

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = s.indicator (fun x => ofReal (g x - f x)) x

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [Measure.prod_apply]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ∫⁻ (x : α), volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)

Tactic:
simp [h, Ioo]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0

Tactic:
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = ∅ := by simp [h]

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ∅
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = 0