awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact lintegral_congr fun x => tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
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∞)
⊢ μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h₃ h₄ :
  Eq (α := ℝ≥0∞) (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (s.indicator 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]

Premises used: MeasureTheory.Measure.restrict_comm, MeasureTheory.lintegral_indicator, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : (μ.restrict s).withDensity 1 = μ.restrict s
rw₁ rw₂ : μ.restrict s = μ.restrict s
⊢ μ.withDensity (s.indicator 1) = μ.restrict s

Tactic:
rw [withDensity_indicator hs, withDensity_one]

Premises used: MeasureTheory.withDensity_one, MeasureTheory.withDensity_indicator
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
⊢ MeasurableSet S

Tactic:
have hS : MeasurableSet S := measurableSet_lt hf measurable_const
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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)

Tactic:
⟨S, hS, ?_, ?_⟩

Premises used: MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
refine_2 :
  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)

Tactic:
refine ⟨S, hS, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
refine_1 : ∀ᵐ (x : α) ∂μ.restrict S, ENNReal.ofReal (f x) = 0 x
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x) : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hS, lintegral_eq_zero_iff hf.ennreal_ofReal, EventuallyEq]

Premises used: MeasureTheory.lintegral_eq_zero_iff, Measurable.ennreal_ofReal, Filter.EventuallyEq, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict S, ENNReal.ofReal (f x) = 0 x

Tactic:
(ae_restrict_mem hS).mono fun x hx => ENNReal.ofReal_eq_zero.2 (le_of_lt hx)

Premises used: Iff.mpr, MeasureTheory.ae_restrict_mem, ENNReal.ofReal_eq_zero, le_of_lt, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict S, ENNReal.ofReal (f x) = 0 x

Tactic:
exact (ae_restrict_mem hS).mono fun x hx => ENNReal.ofReal_eq_zero.2 (le_of_lt hx)

Premises used: Iff.mpr, MeasureTheory.ae_restrict_mem, ENNReal.ofReal_eq_zero, le_of_lt, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
refine_2 : ∀ᵐ (x : α) ∂μ.restrict Sᶜ, ENNReal.ofReal (-f x) = 0 x
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x) : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hS.compl, lintegral_eq_zero_iff hf.neg.ennreal_ofReal, EventuallyEq]

Premises used: MeasureTheory.lintegral_eq_zero_iff, Measurable.ennreal_ofReal, Filter.EventuallyEq, MeasurableSet.compl, Measurable.neg, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict Sᶜ, ENNReal.ofReal (-f x) = 0 x

Tactic:
(ae_restrict_mem hS.compl).mono fun x hx =>
        ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)

Premises used: Iff.mpr, MeasureTheory.ae_restrict_mem, ENNReal.ofReal_eq_zero, neg_pos, mt, MeasurableSet.compl, Filter.Eventually.mono, not_lt, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x : α | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict Sᶜ, ENNReal.ofReal (-f x) = 0 x

Tactic:
exact
      (ae_restrict_mem hS.compl).mono fun x hx =>
        ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)

Premises used: Iff.mpr, MeasureTheory.ae_restrict_mem, ENNReal.ofReal_eq_zero, neg_pos, mt, MeasurableSet.compl, Filter.Eventually.mono, not_lt, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
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∞)
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h₃ h₄ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t ∩ s, f a ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥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]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_restrict, MeasureTheory.withDensity_apply, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
f : α → ℝ≥0∞
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∞)
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h₃ h₄ : ∫⁻ (a : α) in t ∩ s, f a ∂μ = ∫⁻ (a : α) in t ∩ s, f a ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥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]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_restrict, Inter.inter, MeasureTheory.withDensity_apply', MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

Tactic:
@Measure.ext _ m _ _ (fun s hs ↦ ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
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∞)
⊢ (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

Tactic:
refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
rw : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
rw₁ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
rw₂ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
rw₃ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
rw₄ rw₅ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]

Premises used: MeasureTheory.lintegral_trim, MeasureTheory.trim_measurableSet_eq, MeasureTheory.restrict_trim, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
h : μ ⟂ₘ ν
⊢ μ.withDensity f ⟂ₘ ν

Tactic:
MutuallySingular.mono_ac h (withDensity_absolutelyContinuous _ _) AbsolutelyContinuous.rfl

Premises used: MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ f =ᶠ[ae μ] 0
rw₁ : ∫⁻ (a : α) in univ, f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
rw₂ : ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
rw₃ rw₄ : f =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0
⊢ μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]

Premises used: MeasureTheory.lintegral_eq_zero_iff', MeasureTheory.Measure.measure_univ_eq_zero, MeasurableSet.univ, MeasureTheory.withDensity_apply, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
mp :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
mpr :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
mp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))

Premises used: MeasureTheory.Measure.withDensity, Set.inter_subset_inter_right, MeasureTheory.measure_mono_null, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_toMeasurable, hs]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
mp :
  ∀
    (A :
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
mp₁ :
  ∀ (A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x),
    NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [withDensity_apply f (measurableSet_toMeasurable _ s),
      lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
      EventuallyEq, ae_restrict_iff'₀, ae_iff] at A

Premises used: MeasureTheory.lintegral_eq_zero_iff', Filter.EventuallyEq, AEMeasurable.restrict, MeasureTheory.ae_iff, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.ae_restrict_iff'₀, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x
⊢ NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ

Tactic:
simp only [measurableSet_toMeasurable, MeasurableSet.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
A
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
h : {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s = {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
convert! A using 2
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
h :
  ∀ (x : α),
    x ∈ {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s ↔
      Membership.mem (γ := Set α) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} x
⊢ {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s = {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
⊢ x ∈ {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s ↔
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} x

Tactic:
simp only [and_comm, exists_prop, mem_inter_iff, mem_setOf_eq,
      not_forall]

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, and_comm, exists_prop, Classical.not_forall
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
inl : ∀ (fx : f x = 0), x ∈ t ∪ {x : α | f x = 0}
inr : ∀ (fx : f x ≠ 0), x ∈ t ∪ {x : α | f x = 0}
⊢ x ∈ t ∪ {x : α | f x = 0}

Tactic:
rcases eq_or_ne (f x) 0 with (fx | fx)

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x = 0
⊢ x ∈ t ∪ {x : α | f x = 0}

Tactic:
simp only [fx, mem_union, mem_setOf_eq, or_true]

Premises used: Set.mem_union, Set.mem_setOf_eq, or_true
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
inr : x ∈ t
⊢ x ∈ t ∪ {x : α | f x = 0}

Tactic:
left
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
inr : x ∈ {x : α | f x ≠ 0} ∩ s
⊢ x ∈ t

Tactic:
apply subset_toMeasurable _ _

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ {x : α | f x ≠ 0} ∩ s

Tactic:
⟨fx, hx⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ {x : α | f x ≠ 0} ∩ s

Tactic:
exact ⟨fx, hx⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
⊢ s ⊆ t ∪ {x : α | f x = 0}

Tactic:
have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_setOf_eq, or_true]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
apply : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
apply₁ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_mono_null A (measure_union_null _ _)

Premises used: MeasureTheory.measure_union_null, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
a : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply withDensity_absolutelyContinuous

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
a a₁ a₂ a₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable