awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ μ.restrict t = μ.restrict s

Tactic:
exact restrict_toMeasurable_of_sFinite s

Premises used: MeasureTheory.Measure.restrict_toMeasurable_of_sFinite
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
f₁ : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (a : α) in s, f a ∂μ

Tactic:
calc
  μ.withDensity f s ≤ μ.withDensity f t := measure_mono (subset_toMeasurable μ s)
  _ = ∫⁻ a in t, f a ∂μ := withDensity_apply f (measurableSet_toMeasurable μ s)
  _ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sFinite s

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.subset_toMeasurable, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.measure_mono, DFunLike.coe, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((withDensity 0 f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure α) (withDensity 0 f) 0

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
h : ∫⁻ (a : α) in s, f a ∂0 = ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) (((withDensity 0 f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂0 = ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ μ.withDensity f = μ.withDensity g

Tactic:
Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity f = μ.withDensity g

Tactic:
refine Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
lintegral_congr_ae (ae_restrict_of_ae h)

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
exact lintegral_congr_ae (ae_restrict_of_ae h)

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
⊢ μ.withDensity f ≤ μ.withDensity g

Tactic:
le_iff.2 fun s hs ↦ ?_

Premises used: Iff.mpr, MeasureTheory.Measure.le_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    LE.le (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity f ≤ μ.withDensity g

Tactic:
refine le_iff.2 fun s hs ↦ ?_

Premises used: Iff.mpr, MeasureTheory.Measure.le_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
setLIntegral_mono_ae' hs ?_

Premises used: MeasureTheory.setLIntegral_mono_ae'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
refine : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
refine setLIntegral_mono_ae' hs ?_

Premises used: MeasureTheory.setLIntegral_mono_ae'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
x : α
h_le : f x ≤ g x
⊢ x ∈ s → f x ≤ g x

Tactic:
fun _ ↦ h_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ s → f x ≤ g x) x} x}
      a
h₁ h₂ : ∀ (x : α) (h_le : f x ≤ g x), x ∈ s → f x ≤ g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x

Tactic:
filter_upwards [hfg] with x h_le using fun _ ↦ h_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.withDensity f + μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
refine Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f + μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
    ← lintegral_add_left hf]

Premises used: MeasureTheory.Measure.add_apply, MeasureTheory.lintegral_add_left, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ

Tactic:
simp only [Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : Measurable g
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
simpa only [add_comm] using withDensity_add_left hg f

Premises used: MeasureTheory.withDensity_add_left, add_comm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((μ + ν).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.withDensity f + ν.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ + ν).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f + ν.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [withDensity_apply f hs, restrict_add, lintegral_add_measure, Measure.add_apply]

Premises used: MeasureTheory.lintegral_add_measure, MeasureTheory.Measure.restrict_add, MeasureTheory.Measure.add_apply, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sum fun (n : ι) ↦ (μ n).withDensity f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (sum μ).withDensity f = sum fun (n : ι) ↦ (μ n).withDensity f

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h₂ : (∫⁻ (a : α), f a ∂sum fun (i : ι) ↦ (μ i).restrict s) = ∑' (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∞)

Tactic:
simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.restrict_sum, MeasureTheory.lintegral_sum_measure, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
refine Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul r hf]

Premises used: MeasureTheory.Measure.coe_smul, smul_eq_mul, MeasureTheory.lintegral_const_mul, MeasureTheory.withDensity_apply, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Premises used: smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
refine Measure.ext fun s hs => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (r • f) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul' r f hr]

Premises used: MeasureTheory.lintegral_const_mul', MeasureTheory.Measure.coe_smul, smul_eq_mul, MeasureTheory.withDensity_apply, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Premises used: smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((r • μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (r • μ).withDensity f = r • μ.withDensity f

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((r • μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((r • μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [withDensity_apply, hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
rwa : ∫⁻ (a : α) in univ, f a ∂μ < ∞
rwa₁ : ∫⁻ (a : α), f a ∂μ < ∞
rwa₂ rwa₃ rwa₄ rwa₅ : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, MeasurableSet.univ, MeasureTheory.withDensity_apply, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ μ.withDensity f ≪ μ

Tactic:
AbsolutelyContinuous.mk fun s hs₁ hs₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
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∞)
⊢ μ.withDensity f ≪ μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs₁ hs₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : ∫⁻ (a : α) in s, f a ∂μ = 0
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs₁]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0

Tactic:
setLIntegral_measure_zero _ _ hs₂

Premises used: MeasureTheory.setLIntegral_measure_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0

Tactic:
exact setLIntegral_measure_zero _ _ hs₂

Premises used: MeasureTheory.setLIntegral_measure_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s μ
t : Set α := toMeasurable μ s
⊢ ∫⁻ (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
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ∂μ
⊢ 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)
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
rw : (μ.withDensity f : (a : Set α) → ℝ≥0∞) t = ∫⁻ (a : α) in t, f a ∂μ
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [← A, ← B]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) t = ∫⁻ (a : α) in t, f a ∂μ

Tactic:
withDensity_apply _ (measurableSet_toMeasurable μ s)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) t = ∫⁻ (a : α) in t, f a ∂μ

Tactic:
exact withDensity_apply _ (measurableSet_toMeasurable μ s)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity 0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity 0 = 0

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity 0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity 1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity 1 = μ

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity 1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ c : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ.withDensity fun (x : α) ↦ c) = c • μ

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ c : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
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∞)
⊢ μ.withDensity (∑' (n : ι), f n) = sum fun (n : ι) ↦ μ.withDensity (f n)

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
h₁ : ∫⁻ (a : α) in s, (∑' (n : ι), f n) a ∂μ = ∑' (i : ι), ∫⁻ (a : α) in s, f i a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (∑' (n : ι), f n) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ μ.withDensity (f n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [sum_apply _ hs, withDensity_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
h₁ : ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∫⁻ (a : α) in s, ∑' (i : ι), f i a ∂μ
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∑' (i : ι), ∫⁻ (x : α) in s, f i x ∂μ

Tactic:
rw [← lintegral_tsum fun i => (h i).aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ∂μ = ∫⁻ (a : α) in s, ∑' (i : ι), f i a ∂μ

Tactic:
lintegral_congr fun x => tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Premises used: Iff.mpr, ENNReal.summable, tsum_apply, MeasureTheory.lintegral_congr, Pi.summable