awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have 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∞)
Tactic: rw [lintegral_congr_ae h₁, ←
    volume_regionBetween_eq_lintegral' hf.measurable_mk hg.measurable_mk hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞) (((μ.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∞)
have 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∞)
Tactic: convert! h₂ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: convert! h₂ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞) (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
    ((((μ.restrict s).prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) : ℝ≥0∞)
have 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∞)
Tactic: rw [Measure.restrict_prod_eq_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
    (((μ.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∞)
have h : Eq (α := ℝ≥0∞)
  (((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
      (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
    ℝ≥0∞)
  (((Measure.restrict (μ.prod volume) (SProd.sprod (β := Set ℝ) s univ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞)
      (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) :
    ℝ≥0∞)
Tactic: rw [Measure.restrict_prod_eq_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : 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 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)
have refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.lt✝ (f p.1) p.2) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.lt✝ (f p.1) p.2) (μ.prod volume)
⊢ NullMeasurableSet (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)
have refine_2 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.lt✝ p.2 (g p.1)) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ AEMeasurable (β := ℝ) (_m := Prod.instMeasurableSpace) (fun (p : α × ℝ) ↦ f p.1) (μ.prod volume)
have funProp : inst ≤ inst
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
funProp : inst ≤ inst
⊢ AEMeasurable (β := ℝ) (_m := Prod.instMeasurableSpace) (fun (p : α × ℝ) ↦ f p.1) (μ.prod volume)
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (p0 : α) ↦ f p0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ) fun (p0 : α) ↦ f p0
⊢ AEMeasurable (β := ℝ) (_m := Prod.instMeasurableSpace) (fun (p : α × ℝ) ↦ f p.1) (μ.prod volume)
have funProp₂ : Measure.map (fun (p : α × ℝ) ↦ p.1) (μ.prod volume) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ AEMeasurable (β := ℝ) (_m := Prod.instMeasurableSpace) (fun (p : α × ℝ) ↦ g p.1) (μ.prod volume)
have funProp : inst ≤ inst
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
funProp : inst ≤ inst
⊢ AEMeasurable (β := ℝ) (_m := Prod.instMeasurableSpace) (fun (p : α × ℝ) ↦ g p.1) (μ.prod volume)
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (p0 : α) ↦ g p0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ) fun (p0 : α) ↦ g p0
⊢ AEMeasurable (β := ℝ) (_m := Prod.instMeasurableSpace) (fun (p : α × ℝ) ↦ g p.1) (μ.prod volume)
have funProp₂ : Measure.map (fun (p : α × ℝ) ↦ p.1) (μ.prod volume) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : 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 ∈ Ioc (f p.1) (g p.1)} (μ.prod volume)
have refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.lt✝ (f p.1) p.2) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.lt✝ (f p.1) p.2) (μ.prod volume)
⊢ NullMeasurableSet (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)} (μ.prod volume)
have refine_2 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.le✝ p.2 (g p.1)) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ Eq.{u_1 + 1} (α := Set (α × ℝ)) {p : α × ℝ | p.2 ≤ g p.1} {p : α × ℝ | g p.1 < p.2}ᶜ
have h : ∀ (p : α × ℝ),
  Membership.mem (γ := Set (α × ℝ)) {p : α × ℝ | p.2 ≤ g p.1} p ↔
    Membership.mem (γ := Set (α × ℝ)) {p : α × ℝ | g p.1 < p.2}ᶜ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : 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)
have refine_2 : NullMeasurableSet (α := α × ℝ) {p : α × ℝ | g p.1 < p.2}ᶜ (μ.prod volume)
Tactic: rw [show {p : α × ℝ | p.snd ≤ g p.fst} = {p : α × ℝ | g p.fst < p.snd}ᶜ by
          ext p
          simp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : 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 ∈ Ico (f p.1) (g p.1)} (μ.prod volume)
have refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.le✝ (f p.1) p.2) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.le✝ (f p.1) p.2) (μ.prod volume)
⊢ NullMeasurableSet (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)} (μ.prod volume)
have refine_2 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.lt✝ p.2 (g p.1)) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ Eq.{u_1 + 1} (α := Set (α × ℝ)) {p : α × ℝ | f p.1 ≤ p.2} {p : α × ℝ | p.2 < f p.1}ᶜ
have h : ∀ (p : α × ℝ),
  Membership.mem (γ := Set (α × ℝ)) {p : α × ℝ | f p.1 ≤ p.2} p ↔
    Membership.mem (γ := Set (α × ℝ)) {p : α × ℝ | p.2 < f p.1}ᶜ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : 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)
have refine_1 : NullMeasurableSet (α := α × ℝ) {p : α × ℝ | p.2 < f p.1}ᶜ (μ.prod volume)
Tactic: rw [show {p : α × ℝ | f p.fst ≤ p.snd} = {p : α × ℝ | p.snd < f p.fst}ᶜ by
          ext p
          simp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : 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)
have refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.le✝ (f p.1) p.2) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
refine_1 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.le✝ (f p.1) p.2) (μ.prod volume)
⊢ NullMeasurableSet (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)} (μ.prod volume)
have refine_2 : NullMeasurableSet (α := α × ℝ) (fun (p : α × ℝ) ↦ Real.le✝ p.2 (g p.1)) (μ.prod volume)
Tactic: refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
have hfinite : (s \ u).Finite
Tactic: have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
have obtain : ∀ (A : Set ((↑s : Type) × (↑s : Type))) (A_count : A.Countable)
  (hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)), ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
Tactic: obtain ⟨A, A_count, hA⟩ :
    ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
    isOpen_iUnion_countable _ fun p => isOpen_Ioo
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
have pos : ∀ (h'x : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x), x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
Tactic: by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
pos : ∀ (h'x : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x), x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
have neg : ∀ (h'x : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i), x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
Tactic: by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
h'x : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
have h'x₁ : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
Tactic: rw [← hA] at h'x
Cleared hypotheses: h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
h'x : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
have pos : ∀ (p : (↑s : Type) × (↑s : Type)) (pA : p ∈ A) (xp : x ∈ T p), x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
Tactic: obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
        simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p_1 : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p_1 x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
x : ℝ
hx : x ∈ s
h'x : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
p : (↑s : Type) × (↑s : Type)
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p
have pos : Membership.mem (γ := Set ℝ) (⋃ p ∈ A, s ∩ T p) x
Tactic: right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
have this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
Tactic: have : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p := by
    intro x hx
    by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
    · rw [← hA] at h'x
      obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
        simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
      right
      exact mem_biUnion pA ⟨hx, xp⟩
    · exact Or.inl ⟨hx, h'x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
have apply : ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u ∪ ⋃ p ∈ A, s ∩ T p), p x
Tactic: apply ae_restrict_of_ae_restrict_of_subset this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u ∪ ⋃ p ∈ A, s ∩ T p), p x
have rw : (∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
Tactic: rw [ae_restrict_union_iff, ae_restrict_biUnion_iff _ A_count]