-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_apply_eq_zero' {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f μ) :
    μ.withDensity f s = 0 ↔ μ ({ x | f x ≠ 0 } ∩ s) = 0

Proof state:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x
⊢ NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ

Tactic:
swap

Result:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x
⊢ NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ

case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 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, eq_self_iff_true, or_true]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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

Result:
no goals

Proof state:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]

Result:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : (μ.withDensity f) t = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Proof state:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
simp only [Pi.zero_apply, mem_setOf_eq, Filter.mem_mk] at A

Result:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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
⊢ {x | f x = 0} a

Tactic:
rw [h] at ha

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ s ⊆ t ∪ {x | f x = 0}

Tactic:
intro x hx

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
⊢ x ∈ t ∪ {x | f x = 0}

Proof state:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
⊢ (μ.withDensity f) s = 0

Tactic:
let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)

Result:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ (μ.withDensity f) s = 0

Proof state:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
convert A using 2

Result:
case h.e'_2.h.e'_6
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} = 0
⊢ {x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s = {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)}

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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
t : {x | f x = 0} =ᶠ[ae (μ.withDensity f)] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ (μ.withDensity g) {x | g x = 0} = 0

Tactic:
rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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
t : {x | f x = 0} =ᶠ[ae (μ.withDensity f)] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ g =ᶠ[ae (μ.restrict {x | g x = 0})] 0

Proof state:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ (μ.withDensity f) s = 0 → μ ({x | f x ≠ 0} ∩ s) = 0

Tactic:
intro hs

Result:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
⊢ μ ({x | f x ≠ 0} ∩ s) = 0

Proof state:
case inr.h.a
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 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⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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
t : {x | f x = 0} =ᶠ[ae (μ.withDensity f)] {x | g x = 0}
⊢ (μ.withDensity g) {x | g x = 0} = 0

Tactic:
have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 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
t : {x | f x = 0} =ᶠ[ae (μ.withDensity f)] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ (μ.withDensity g) {x | g x = 0} = 0