awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
this this₁ this₂ :
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have this₃ : let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det),
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
Tactic: classical
    -- this is deduced from the matrix case
    let M := LinearMap.toMatrix' f
    have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
    have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
    rw [A, B]
    apply map_matrix_volume_pi_eq_smul_volume_pi
    rwa [A] at hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
this this₁ this₂ :
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₃ :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det),
    Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have this₄ : let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
  (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M),
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
Tactic: classical
    -- this is deduced from the matrix case
    let M := LinearMap.toMatrix' f
    have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
    have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
    rw [A, B]
    apply map_matrix_volume_pi_eq_smul_volume_pi
    rwa [A] at hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
this this₁ this₂ :
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₃ :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det),
    Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₄ :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
    (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M),
    Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have this₅ : let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
  (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M),
  Measure.map (α := ι → ℝ)
      (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
Tactic: classical
    -- this is deduced from the matrix case
    let M := LinearMap.toMatrix' f
    have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
    have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
    rw [A, B]
    apply map_matrix_volume_pi_eq_smul_volume_pi
    rwa [A] at hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
this this₁ this₂ :
  Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₃ :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det),
    Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₄ :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
    (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M),
    Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
this₅ :
  let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
  ∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
    (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M),
    Measure.map (α := ι → ℝ)
        (⇑((toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) volume =
      HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |M.det⁻¹|) volume
⊢ Measure.map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) volume =
    HSMul.hSMul (β := Measure (ι → ℝ)) (ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|) volume
have hM : let M : Matrix ι ι ℝ := (LinearMap.toMatrix' : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → Matrix ι ι ℝ) f;
∀ (A : (LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f = M.det)
  (B : f = (toLin' : (a : Matrix ι ι ℝ) → (ι → ℝ) →ₗ[ℝ] ι → ℝ) M), M.det ≠ 0
Tactic: classical
    -- this is deduced from the matrix case
    let M := LinearMap.toMatrix' f
    have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
    have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
    rw [A, B]
    apply map_matrix_volume_pi_eq_smul_volume_pi
    rwa [A] at hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
have 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})
Tactic: dsimp only [regionBetween, Ioo, mem_setOf_eq, setOf_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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})
have measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
Tactic: refine
    MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)}
have 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})
Tactic: dsimp only [regionBetween, Ioc, mem_setOf_eq, setOf_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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})
have measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
Tactic: refine
    MeasurableSet.inter ?_
      ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)}
have 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})
Tactic: dsimp only [regionBetween, Ico, mem_setOf_eq, setOf_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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})
have measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
Tactic: refine
    MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)}
have 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})
Tactic: dsimp only [regionBetween, Icc, mem_setOf_eq, setOf_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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})
have measurable_snd : MeasurableSet.{u_1} (α := α × ℝ) {a : α × ℝ | a.1 ∈ s}
Tactic: refine
    MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_le measurable_snd (hg.comp measurable_fst)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have rw : ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
  ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
Tactic: rw [Measure.prod_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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) ∂μ
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have rw₁ : MeasurableSet (regionBetween f g s)
Tactic: rw [Measure.prod_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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))
have 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∞)
Tactic: funext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
have pos : ∀ (h : x ∈ s), (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
have neg : ∀ (h : x ∉ s), Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
α : 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 : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
have hx : {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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
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 (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} : ℝ≥0∞) (0 : ℝ≥0∞)
have hx : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have 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))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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))
⊢ ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' regionBetween f g s) ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have dsimp : ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ =
  ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
Tactic: dsimp only [regionBetween, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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))
⊢ ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) {a : ℝ | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have rw : ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
Tactic: rw [h, lintegral_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have rw : ∫⁻ (x : α), (volume : (a : Set ℝ) → ℝ≥0∞) (Prod.mk x ⁻¹' 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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) ∂μ
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have rw₁ : MeasurableSet (regionBetween f g s)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
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
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have h₁ : (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
-- 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)
⊢ 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∞)
have H : regionBetween f g s =ᶠ[ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)]
  regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s
Tactic: apply measure_congr
-- 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)
⊢ regionBetween f g s =ᶠ[ae (F := Measure (α × ℝ)) ((μ.restrict s).prod volume)]
    regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s
have 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
Tactic: apply EventuallyEq.rfl.inter
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
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)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) (regionBetween f g s) =
    ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
have 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∞)
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)