awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (i : ι), ((μ i).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ (μ n).withDensity f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (a : α) in s, f a ∂sum μ = ∑' (i : ι), ∫⁻ (a : α) in s, f a ∂μ i
Tactic: simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (i : ι), ((μ i).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ : ∫⁻ (a : α) in s, f a ∂sum μ = ∑' (i : ι), ∫⁻ (a : α) in s, f a ∂μ i
⊢ Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ (μ n).withDensity f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : (∫⁻ (a : α), f a ∂sum fun (i : ι) ↦ (μ i).restrict s) = ∑' (i : ι), ∫⁻ (a : α) in s, f a ∂μ i
Tactic: simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ μ.withDensity (r • f) = r • μ.withDensity f
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine Measure.ext fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
Tactic: rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul r hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
⊢ μ.withDensity (r • f) = r • μ.withDensity f
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine Measure.ext fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
Tactic: rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul' r f hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (r • μ).withDensity f = r • μ.withDensity f
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((r • μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.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 α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa : ∫⁻ (a : α) in univ, f a ∂μ < ∞
Tactic: rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
rwa : ∫⁻ (a : α) in univ, f a ∂μ < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa₁ : ∫⁻ (a : α), f a ∂μ < ∞
Tactic: rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ μ.withDensity f ≪ μ
have refine : ∀ (s : Set α) (hs₁ : MeasurableSet s) (hs₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun s hs₁ hs₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, f a ∂μ = 0
Tactic: rw [withDensity_apply _ hs₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s μ
t : Set α := toMeasurable μ s
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
have A : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: have A : ∫⁻ a in t, f a ∂μ = ∫⁻ a in s, f a ∂μ :=
    setLIntegral_congr hs.toMeasurable_ae_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s μ
t : Set α := toMeasurable μ s
A : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
have B : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have B : μ.withDensity f t = μ.withDensity f s :=
    measure_congr (withDensity_absolutelyContinuous μ f hs.toMeasurable_ae_eq)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s μ
t : Set α := toMeasurable μ s
A : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
B : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
have rw : (μ.withDensity f : (a : Set α) → ℝ≥0∞) t = ∫⁻ (a : α) in t, f a ∂μ
Tactic: rw [← A, ← B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.withDensity 0 = 0
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity 0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.withDensity 1 = μ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity 1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ (μ.withDensity fun (x : α) ↦ c) = c • μ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ c : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ μ.withDensity (∑' (n : ι), f n) = sum fun (n : ι) ↦ μ.withDensity (f n)
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (∑' (n : ι), f n) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ μ.withDensity (f n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (∑' (n : ι), f n) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ μ.withDensity (f n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (a : α) in s, (∑' (n : ι), f n) a ∂μ = ∑' (i : ι), ∫⁻ (a : α) in s, f i a ∂μ
Tactic: simp_rw [sum_apply _ hs, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∑' (i : ι), ∫⁻ (x : α) in s, f i x ∂μ
have h₁ : ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∫⁻ (a : α) in s, ∑' (i : ι), f i a ∂μ
Tactic: rw [← lintegral_tsum fun i => (h i).aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f
have h : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) ((μ.withDensity (s.indicator f) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (s.indicator f) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : ∫⁻ (a : α) in t, s.indicator f a ∂μ = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
Tactic: rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
    withDensity_apply _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h : ∫⁻ (a : α) in t, s.indicator f a ∂μ = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (s.indicator f) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
Tactic: rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
    withDensity_apply _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h : ∫⁻ (a : α) in t, s.indicator f a ∂μ = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
h₁ : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (s.indicator f) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₂ : ∫⁻ (a : α) in t, f a ∂μ.restrict s = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
Tactic: rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
    withDensity_apply _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h : ∫⁻ (a : α) in t, s.indicator f a ∂μ = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
h₁ : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
h₂ : ∫⁻ (a : α) in t, f a ∂μ.restrict s = ((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (s.indicator f) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
    withDensity_apply _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.withDensity (s.indicator 1) = μ.restrict s
have rw : (μ.restrict s).withDensity 1 = μ.restrict s
Tactic: rw [withDensity_indicator hs, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : (μ.restrict s).withDensity 1 = μ.restrict s
⊢ μ.withDensity (s.indicator 1) = μ.restrict s
have rw₁ : μ.restrict s = μ.restrict s
Tactic: rw [withDensity_indicator hs, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
⊢ (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
have hS : MeasurableSet S
Tactic: have hS : MeasurableSet S := measurableSet_lt hf measurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
have refine_1 : Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨S, hS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
refine_1 : Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
have refine_2 : Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x) : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨S, hS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∀ᵐ (x : α) ∂μ.restrict S, ENNReal.ofReal (f x) = 0 x
Tactic: rw [withDensity_apply _ hS, lintegral_eq_zero_iff hf.ennreal_ofReal, EventuallyEq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x) : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : ∀ᵐ (x : α) ∂μ.restrict Sᶜ, ENNReal.ofReal (-f x) = 0 x
Tactic: rw [withDensity_apply _ hS.compl, lintegral_eq_zero_iff hf.neg.ennreal_ofReal, EventuallyEq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f
have h : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
  (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₂ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t, f a ∂μ.restrict s
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
h₂ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t, f a ∂μ.restrict s
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₃ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t ∩ s, f a ∂μ
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f
have h : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
  (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₂ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t, f a ∂μ.restrict s
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
h₂ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t, f a ∂μ.restrict s
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₃ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t ∩ s, f a ∂μ
Tactic: rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
    restrict_restrict ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).trim hm = (μ.trim hm).withDensity f
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
Tactic: rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]