awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
refine_2 : ∀ (x : α), x ∈ spanningSets μ (max (spanningSetsIndex μ x) ⌈f x⌉₊)
⊢ ∀ (x : α), ∃ (i : ℕ), x ∈ spanningSets μ i ∩ f ⁻¹' Iic (↑i : ℝ≥0)
have refine_2₁ : ∀ (x : α), x ∈ f ⁻¹' Iic (↑(max (spanningSetsIndex μ x) ⌈f x⌉₊) : ℝ≥0)
Tactic: refine fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ SigmaFinite (μ.withDensity f)
have this : f =ᶠ[ae μ] fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)
Tactic: have : f =ᵐ[μ] fun x ↦ (f x).toNNReal := hf_ne_top.mono fun x hx ↦ (ENNReal.coe_toNNReal hx).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : f =ᶠ[ae μ] fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)
⊢ SigmaFinite (μ.withDensity f)
have rw : SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞))
Tactic: rw [withDensity_congr_ae this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
have obtain : ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hgf : g ≤ f)
  (hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
Tactic: obtain ⟨g, hgm, hgf, hint⟩ := exists_measurable_le_forall_setLIntegral_eq μ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
have right : μ.withDensity g = μ.withDensity f
Tactic: use g, hgm, hgf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ μ.withDensity g = μ.withDensity f
have right : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
⊢ SFinite (μ.withDensity f)
have inr : ∀ (this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)) (hfm : ¬Measurable f),
  SFinite (μ.withDensity f)
Tactic: wlog hfm : Measurable f generalizing f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
inr :
  ∀ (this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)) (hfm : ¬Measurable f),
    SFinite (μ.withDensity f)
⊢ SFinite (μ.withDensity f)
have wlog : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)
Tactic: wlog hfm : Measurable f generalizing f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)
hfm : ¬Measurable f
⊢ SFinite (μ.withDensity f)
have inr : ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (h : μ.withDensity g = μ.withDensity f), SFinite (μ.withDensity f)
Tactic: rcases exists_measurable_le_withDensity_eq μ f with ⟨g, hgm, -, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
⊢ SFinite (μ.withDensity f)
have inr : ∀ (this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)) (hμ : ¬IsFiniteMeasure μ),
  SFinite (μ.withDensity f)
Tactic: wlog hμ : IsFiniteMeasure μ generalizing μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
inr :
  ∀ (this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f))
    (hμ : ¬IsFiniteMeasure μ), SFinite (μ.withDensity f)
⊢ SFinite (μ.withDensity f)
have wlog : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
Tactic: wlog hμ : IsFiniteMeasure μ generalizing μ
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ SFinite (μ.withDensity f)
have inr : SFinite.{u_1} (α := α) (m0 := m0) (sum fun (n : ℕ) ↦ (sfiniteSeq μ n).withDensity f)
Tactic: rw [← sum_sfiniteSeq μ, withDensity_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ SFinite.{u_1} (α := α) (m0 := m0) (sum fun (n : ℕ) ↦ (sfiniteSeq μ n).withDensity f)
have this₁ : ∀ (n : ℕ), SFinite ((sfiniteSeq μ n).withDensity f)
Tactic: have (n : ℕ) : SFinite ((sfiniteSeq μ n).withDensity f) := this inferInstance
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
⊢ SFinite (μ.withDensity f)
have hs : MeasurableSet s
Tactic: have hs : MeasurableSet s := hfm (measurableSet_singleton _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
have rw : μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
  μ.withDensity (sᶜ.indicator f) + μ.withDensity (∑' (n : ℕ), s.indicator 1)
Tactic: rw [← withDensity_tsum (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + μ.withDensity (∑' (n : ℕ), s.indicator 1)
have e_a : ∀ (x : α), s.indicator f x = (∑' (n : ℕ), s.indicator 1) x
Tactic: congr 2 with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
⊢ s.indicator f x = (∑' (n : ℕ), s.indicator 1) x
have e_a : s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
Tactic: rw [ENNReal.tsum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
have if : ∀ (hx : x ∈ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
Tactic: if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
if : ∀ (hx : x ∈ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
have if₁ : ∀ (hx : x ∉ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
Tactic: if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
⊢ SFinite (μ.withDensity f)
have key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
Tactic: have key := calc
    μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) := by
      simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]
    _ = μ.withDensity (sᶜ.indicator f) + .sum fun _ : ℕ ↦ μ.withDensity (s.indicator 1) := by
      rw [← withDensity_tsum (by measurability)]
      congr 2 with x
      rw [ENNReal.tsum_apply]
      if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
⊢ SigmaFinite (μ.withDensity (sᶜ.indicator f))
have refine : ∀ (x : α) (hx : sᶜ.indicator f x = ∞), False
Tactic: refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
⊢ SFinite (μ.withDensity f)
have this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
Tactic: have : SigmaFinite (μ.withDensity (sᶜ.indicator f)) := by
    refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_
    simp [indicator_apply, ite_eq_iff, s] at hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite (μ.withDensity (s.indicator 1))
have rw : SigmaFinite ((μ.restrict s).withDensity 1)
Tactic: rw [withDensity_indicator hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SFinite (μ.withDensity f)
have this₁ : SigmaFinite (μ.withDensity (s.indicator 1))
Tactic: have : SigmaFinite (μ.withDensity (s.indicator 1)) := by
    rw [withDensity_indicator hs]
    exact SigmaFinite.withDensity 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this_1 : SigmaFinite (μ.withDensity (sᶜ.indicator f))
this : SigmaFinite (μ.withDensity (s.indicator 1))
⊢ SFinite (μ.withDensity f)
have rw : SFinite (μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1))
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℝ≥0∞
⊢ SFinite (c • μ)
have rw : SFinite (μ.withDensity fun (x : α) ↦ c)
Tactic: rw [← withDensity_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
⊢ SFinite μ
have rw : SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ))
Tactic: rw [← Measure.restrict_add_restrict_compl (μ := μ) measurableSet_sigmaFiniteSetWRT,
    restrict_compl_sigmaFiniteSetWRT hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
⊢ SFinite μ
have obtain : ∀ (s : Set α)
  (h :
    μ =
      sum fun (x : (↑s : Type u_1)) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
          (dirac (↑x : α))),
  SFinite μ
Tactic: obtain ⟨s, h⟩ := exists_sum_smul_dirac μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
s : Set α
h :
  μ =
    sum fun (x : (↑s : Type u_1)) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
        (dirac (↑x : α))
⊢ SFinite μ
have rw : SFinite.{u_1} (α := α) (m0 := m0)
  (sum fun (x : (↑s : Type u_1)) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
      (dirac (↑x : α)))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
have refine : ∀ (φ : α × β → ℝ≥0∞) (hφ : Measurable φ),
  ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
Tactic: refine ext_of_lintegral _ fun φ hφ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
have rw : ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
  ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
    lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ
⊢ ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
have hf₁ : AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
    lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ
hf₁ : AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
⊢ ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
have rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
    lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ
hf₁ : AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
⊢ ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
have rw₂ : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
    lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ
have refine : ∀ (x : α),
  HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν
Tactic: refine lintegral_congr (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν
have rw : ∫⁻ (a : β), f x * φ (x, a) ∂ν = ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν
Tactic: rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
have funProp : m0 ≤ m0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : m0 ≤ m0
⊢ AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : m0 ≤ m0
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
⊢ AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
have funProp₂ : Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) ≪ μ
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
have funProp : m0 ≤ m0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : m0 ≤ m0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : m0 ≤ m0
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
have funProp₂ : Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) ≪ μ
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
⊢ μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ g z.2
have refine : ∀ (φ : α × β → ℝ≥0∞) (hφ : Measurable φ),
  ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ g z.2
Tactic: refine ext_of_lintegral _ fun φ hφ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ g z.2
have rw : ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ =
  ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν ∂μ
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable,
    lintegral_prod]