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

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [lintegral_congr_ae h₁, ←
  volume_regionBetween_eq_lintegral' hf.measurable_mk hg.measurable_mk hs]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) =
    (μ.prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)

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

Tactic:
have h₁ :
  (fun y => ENNReal.ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y =>
    ENNReal.ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y) :=
  (hg.ae_eq_mk.sub hf.ae_eq_mk).fun_comp ENNReal.ofReal

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
have h₂ :
  (μ.restrict s).prod volume (regionBetween f g s) =
    (μ.restrict s).prod volume
      (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) := by
  apply measure_congr
  apply EventuallyEq.rfl.inter
  exact
    ((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
      (EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Proof state:
case h.e'_2
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ((μ.restrict s).prod volume) (regionBetween f g s)

Tactic:
rw [Measure.restrict_prod_eq_prod_univ]

Result:
case h.e'_2
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ((μ.prod volume).restrict (s ×ˢ univ)) (regionBetween f g s)

Proof state:
case H
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (fun p => Ioo (f p.1) (g p.1) p.2) =ᶠ[ae ((μ.restrict s).prod volume)] fun p =>
    Ioo (AEMeasurable.mk f hf p.1) (AEMeasurable.mk g hg p.1) p.2

Tactic:
exact
  ((quasiMeasurePreserving_fst.ae_eq_comp hf.ae_eq_mk).comp₂ _ EventuallyEq.rfl).inter
    (EventuallyEq.rfl.comp₂ _ <| quasiMeasurePreserving_fst.ae_eq_comp hg.ae_eq_mk)

Result:
no goals