awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
rcases :
  ∀ (g : α → ℝ≥0∞) (hg : Measurable g) (hfg : f =ᶠ[ae μ] g),
    Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases hf with ⟨g, hg, hfg⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
h : ∀ (a : α) (ha : f a = g a), {x : α | f x = 0} a = {x : α | g x = 0} a
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ {x : α | f x = 0} x = {x : α | g x = 0} x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
filter_upwards [hfg] with a ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | f x = 0} a ↔ {x : α | g x = 0} a
⊢ {x : α | f x = 0} a = {x : α | g x = 0} a

Tactic:
rw [eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | f x = 0} a
⊢ 0 = g a

Tactic:
rw [h] at ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | f x = 0} a
ha₁ : 0 = g a
⊢ {x : α | f x = 0} a

Tactic:
rw [h] at ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : 0 = g a
h : {x : α | f x = 0} a
⊢ {x : α | g x = 0} a

Tactic:
ha.symm

Premises used: setOf, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : 0 = g a
h : {x : α | f x = 0} a
⊢ {x : α | g x = 0} a

Tactic:
exact ha.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | g x = 0} a
⊢ f a = 0

Tactic:
rw [h] at ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | g x = 0} a
ha₁ : f a = 0
⊢ {x : α | g x = 0} a

Tactic:
rw [h] at ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = 0
h : {x : α | g x = 0} a
⊢ {x : α | f x = 0} a

Tactic:
ha

Premises used: setOf
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = 0
h : {x : α | g x = 0} a
⊢ {x : α | f x = 0} a

Tactic:
exact ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
⊢ {x : α | f x = 0} a ↔ {x : α | g x = 0} a

Tactic:
exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
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}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}

Tactic:
have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} := by
      apply withDensity_absolutelyContinuous
      filter_upwards [hfg] with a ha
      rw [eq_iff_iff]
      exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
rw : Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) {x : α | g x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_congr t, withDensity_congr_ae hfg]

Premises used: MeasureTheory.measure_congr, MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
⊢ MeasurableSet.{u_1} (α := α) {x : α | g x = 0}

Tactic:
have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
M : MeasurableSet.{u_1} (α := α) {x : α | g x = 0}
rw : g =ᶠ[ae (μ.restrict {x : α | g x = 0})] 0
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) {x : α | g x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]

Premises used: MeasureTheory.lintegral_eq_zero_iff, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
M : MeasurableSet.{u_1} (α := α) {x : α | g x = 0}
h : ∀ (a : α), g a = 0 → g a = 0 a
⊢ g =ᶠ[ae (μ.restrict {x : α | g x = 0})] 0

Tactic:
filter_upwards [ae_restrict_mem M]

Premises used: MeasureTheory.ae_restrict_mem
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
M : MeasurableSet.{u_1} (α := α) {x : α | g x = 0}
⊢ ∀ (a : α), g a = 0 → g a = 0 a

Tactic:
simp only [imp_self, Pi.zero_apply, imp_true_iff]

Premises used: Pi.zero_apply, imp_true_iff, imp_self
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
⊢ 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:
withDensity_apply_eq_zero' <| hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.withDensity_apply_eq_zero'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(f a ≠ 0 → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

Tactic:
rw [ae_iff, ae_iff, withDensity_apply_eq_zero' hf, iff_iff_eq]

Premises used: MeasureTheory.withDensity_apply_eq_zero', iff_iff_eq, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
e_a : Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) {a : α | ¬(f a ≠ 0 → p a)}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(f a ≠ 0 → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
e_a :
  ∀ (x : α),
    Membership.mem (γ := Set α) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) x ↔
      Membership.mem (γ := Set α) {a : α | ¬(f a ≠ 0 → p a)} x
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) {a : α | ¬(f a ≠ 0 → p a)}

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

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

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop, Classical.not_forall
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

Tactic:
ae_withDensity_iff' <| hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.ae_withDensity_iff'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) {x : α | f x ≠ 0} x → p x
rw₁ : NullMeasurableSet {x : α | f x ≠ 0} μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}, p x

Tactic:
rw [ae_withDensity_iff' hf, ae_restrict_iff'₀]

Premises used: MeasureTheory.ae_withDensity_iff', MeasureTheory.ae_restrict_iff'₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) {x : α | f x ≠ 0} x → p x

Tactic:
simp only [mem_setOf]

Premises used: Set.mem_setOf
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rcases : ∀ (g : α → ℝ≥0∞) (hg : Measurable g) (hfg : f =ᶠ[ae μ] g), NullMeasurableSet {x : α | f x ≠ 0} μ
⊢ NullMeasurableSet {x : α | f x ≠ 0} μ

Tactic:
rcases hf with ⟨g, hg, hfg⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
h : ∀ (a : α) (ha : f a = g a), {x : α | g x ≠ 0} a = {x : α | f x ≠ 0} a
⊢ {x : α | g x ≠ 0} =ᶠ[ae μ] {x : α | f x ≠ 0}

Tactic:
filter_upwards [hfg] with a ha
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | g x ≠ 0} a ↔ {x : α | f x ≠ 0} a
⊢ {x : α | g x ≠ 0} a = {x : α | f x ≠ 0} a

Tactic:
simp only [eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : g a ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : f a ≠ 0), {x : α | f x ≠ 0} a
⊢ {x : α | f x ≠ 0} a

Tactic:
rwa [← ha] at h
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : f a ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : g a ≠ 0), {x : α | g x ≠ 0} a
⊢ {x : α | g x ≠ 0} a

Tactic:
rwa [ha] at h
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
⊢ {x : α | g x ≠ 0} a ↔ {x : α | f x ≠ 0} a

Tactic:
exact ⟨fun (h : g a ≠ 0) ↦ by rwa [← ha] at h,
             fun (h : f a ≠ 0) ↦ by rwa [ha] at h⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ {x : α | g x ≠ 0} =ᶠ[ae μ] {x : α | f x ≠ 0}

Tactic:
have nonneg_eq_ae : {x | g x ≠ 0} =ᵐ[μ] {x | f x ≠ 0} := by
      filter_upwards [hfg] with a ha
      simp only [eq_iff_iff]
      exact ⟨fun (h : g a ≠ 0) ↦ by rwa [← ha] at h,
             fun (h : f a ≠ 0) ↦ by rwa [ha] at h⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
nonneg_eq_ae : {x : α | g x ≠ 0} =ᶠ[ae μ] {x : α | f x ≠ 0}
⊢ NullMeasurableSet {x : α | f x ≠ 0} μ

Tactic:
NullMeasurableSet.congr
      (MeasurableSet.nullMeasurableSet
        <| hg (measurableSet_singleton _)).compl
      nonneg_eq_ae

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.compl, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
nonneg_eq_ae : {x : α | g x ≠ 0} =ᶠ[ae μ] {x : α | f x ≠ 0}
⊢ NullMeasurableSet {x : α | f x ≠ 0} μ

Tactic:
exact NullMeasurableSet.congr
      (MeasurableSet.nullMeasurableSet
        <| hg (measurableSet_singleton _)).compl
      nonneg_eq_ae

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.compl, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}, p x

Tactic:
ae_withDensity_iff_ae_restrict' <| hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.ae_withDensity_iff_ae_restrict'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ ∃ (f' : α → ℝ≥0), Measurable f' ∧ f =ᶠ[ae μ] f'

Tactic:
have t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f' := hf
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
t : ∃ (f' : α → ℝ≥0), Measurable f' ∧ f =ᶠ[ae μ] f'
rcases :
  ∀ (f' : α → ℝ≥0) (hf'_m : Measurable f') (hf'_ae : f =ᶠ[ae μ] f'),
    AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
      AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ

Tactic:
rcases t with ⟨f', hf'_m, hf'_ae⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
mp :
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
mpr :
  AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ →
    AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
⊢ MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}

Tactic:
have A : MeasurableSet {x | f' x ≠ 0} := hf'_m (measurableSet_singleton _).compl
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ

Tactic:
⟨fun x => f' x * g' x, hf'_m.coe_nnreal_ennreal.smul g'meas, ?_⟩

Premises used: ENNReal.ofNNReal, HMul.hMul, AEMeasurable, Measurable.coe_nnreal_ennreal, And.intro, Measurable.smul, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
mp : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ

Tactic:
refine ⟨fun x => f' x * g' x, hf'_m.coe_nnreal_ennreal.smul g'meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0},
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
mp₁ :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ,
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x

Tactic:
apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, setOf, Ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal] at hg'

Premises used: Filter.EventuallyEq, AEMeasurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
hg'₁ : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
⊢ MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}

Tactic:
rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal] at hg'

Premises used: Filter.EventuallyEq, AEMeasurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f' x ≠ 0} x →
      Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0},
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)

Tactic:
rw [ae_restrict_iff' A]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
h :
  ∀ (a : α) (ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a) (h'a : f a = f' a) (h_a_nonneg : f' a ≠ 0),
    (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f' x ≠ 0} x →
      Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)

Tactic:
filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg