awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 ≤ a_1} ∩ {a_1 : ℝ | a_1 < g a.1}) a.2})

Tactic:
MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Premises used: measurableSet_le, Measurable.comp, measurable_snd, measurableSet_lt, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 ≤ a_1} ∩ {a_1 : ℝ | a_1 < g a.1}) a.2})

Tactic:
refine
    MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Premises used: measurableSet_le, Measurable.comp, measurable_snd, measurableSet_lt, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
dsimp :
  MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 ≤ a_1} ∩ {a_1 : ℝ | a_1 ≤ g a.1}) a.2})
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Icc, mem_setOf_eq, setOf_and]

Premises used: Set.setOf_and, regionBetween, Set.mem_setOf_eq, Set.Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 ≤ a_1} ∩ {a_1 : ℝ | a_1 ≤ g a.1}) a.2})

Tactic:
MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))

Premises used: measurableSet_le, Measurable.comp, measurable_snd, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
⊢ MeasurableSet.{u_1} (α := α × ℝ)
    ({a : α × ℝ | a.1 ∈ s} ∩
      {a : α × ℝ | Membership.mem (γ := Set ℝ) ({a_1 : ℝ | f a.1 ≤ a_1} ∩ {a_1 : ℝ | a_1 ≤ g a.1}) a.2})

Tactic:
refine
    MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))

Premises used: measurableSet_le, Measurable.comp, measurable_snd, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.2 = f p.1}

Tactic:
simpa using measurableSet_region_between_cc hf hf MeasurableSet.univ

Premises used: measurableSet_region_between_cc, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
rw :
  ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
rw₁ : MeasurableSet (regionBetween f g s)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [Measure.prod_apply]

Premises used: MeasureTheory.Measure.prod_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} : ℝ≥0∞)
      (s.indicator (fun (x : α) ↦ ofReal (g x - f x)) x : ℝ≥0∞)
⊢ Eq (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)})
    (s.indicator fun (x : α) ↦ ofReal (g x - f x))

Tactic:
funext x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
pos : ∀ (h : x ∈ s), (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
neg :
  ∀ (h : x ∉ s), Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) {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
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : 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]

Premises used: Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : 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:
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : 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 : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

Tactic:
simp only [hx, Real.volume_Ioo]

Premises used: Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ Eq (α := Set ℝ) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∅

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
⊢ Eq (α := Set ℝ) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∅

Tactic:
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = ∅ := by simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∉ s
hx : Eq (α := Set ℝ) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∅
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [hx, measure_empty]

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ Eq (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)})
    (s.indicator fun (x : α) ↦ ofReal (g x - f x))

Tactic:
have h :
        (fun x => volume { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) }) =
          s.indicator fun x => ENNReal.ofReal (g x - f x) := by
        funext x
        rw [indicator_apply]
        split_ifs with h
        · have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]
          simp only [hx, Real.volume_Ioo]
        · have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = ∅ := by simp [h]
          simp only [hx, measure_empty]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h :
  Eq (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)})
    (s.indicator fun (x : α) ↦ ofReal (g x - f x))
dsimp :
  ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
⊢ ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
dsimp only [regionBetween, preimage_setOf_eq]

Premises used: regionBetween, Set.preimage_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h :
  Eq (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)})
    (s.indicator fun (x : α) ↦ ofReal (g x - f x))
rw : ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
hs₁ : MeasurableSet s
⊢ ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [h, lintegral_indicator]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h :
  Eq (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)})
    (s.indicator fun (x : α) ↦ ofReal (g x - f x))
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
simp only [hs, Pi.sub_apply]

Premises used: Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h :
  Eq (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)})
    (s.indicator fun (x : α) ↦ ofReal (g x - f x))
⊢ MeasurableSet s

Tactic:
simp only [hs, Pi.sub_apply]

Premises used: Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : 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:
measurableSet_regionBetween hf hg hs

Premises used: measurableSet_regionBetween
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : 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

Premises used: measurableSet_regionBetween
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
rw :
  ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
rw₁ : MeasurableSet (regionBetween f g s)
rw₂ :
  ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
rw₃ : MeasurableSet (regionBetween f g s)
rw₄ :
  ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
rw₅ rw₆ : MeasurableSet (regionBetween f g s)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
classical
    rw [Measure.prod_apply]
    · have h :
        (fun x => volume { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) }) =
          s.indicator fun x => ENNReal.ofReal (g x - f x) := by
        funext x
        rw [indicator_apply]
        split_ifs with h
        · have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]
          simp only [hx, Real.volume_Ioo]
        · have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = ∅ := by simp [h]
          simp only [hx, measure_empty]
      dsimp only [regionBetween, preimage_setOf_eq]
      rw [h, lintegral_indicator] <;> simp only [hs, Pi.sub_apply]
    · exact measurableSet_regionBetween hf hg hs

Premises used: regionBetween, MeasureTheory.Measure.prod_apply, Set.preimage_setOf_eq, MeasureTheory.lintegral_indicator, measurableSet_regionBetween, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) 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
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
H :
  regionBetween f g s =ᶠ[ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)]
    regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s
⊢ Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
H :
  (ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)).EventuallyEq (β := Prop)
    (fun (p : α × ℝ) ↦ Ioo (f p.1) (g p.1) p.2) fun (p : α × ℝ) ↦
    Ioo (AEMeasurable.mk f hf p.1) (AEMeasurable.mk g hg p.1) p.2
⊢ regionBetween f g s =ᶠ[ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)]
    regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s

Tactic:
apply EventuallyEq.rfl.inter

Premises used: Filter.EventuallyEq.inter, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)).EventuallyEq (β := Prop)
    (fun (p : α × ℝ) ↦ Ioo (f p.1) (g p.1) p.2) fun (p : α × ℝ) ↦
    Ioo (AEMeasurable.mk f hf p.1) (AEMeasurable.mk g hg p.1) p.2

Tactic:
((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)

Premises used: Set.Mem, setOf, Filter.EventuallyEq.inter, AEMeasurable.mk, Filter.EventuallyEq.comp₂, Set.inter, MeasureTheory.Measure.quasiMeasurePreserving_fst, Classical.choose, MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp, Filter.EventuallyEq.rfl, AEMeasurable.ae_eq_mk, Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ (ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)).EventuallyEq (β := Prop)
    (fun (p : α × ℝ) ↦ Ioo (f p.1) (g p.1) p.2) 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)

Premises used: Filter.EventuallyEq.inter, Filter.EventuallyEq.comp₂, MeasureTheory.Measure.quasiMeasurePreserving_fst, MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp, Filter.EventuallyEq.rfl, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)

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)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (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]

Premises used: volume_regionBetween_eq_lintegral', MeasureTheory.lintegral_congr_ae, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)

Tactic:
h₂
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞)
    (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)

Tactic:
convert! h₂ using 1
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (y : α) ↦ ofReal ((g - f) y)) fun (y : α) ↦
    ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
      ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    (((Measure.restrict (μ.prod volume) (SProd.sprod (β := Set ℝ) s univ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
        (regionBetween f g s) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)

Tactic:
rw [Measure.restrict_prod_eq_prod_univ]

Premises used: MeasureTheory.Measure.restrict_prod_eq_prod_univ