-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem ae_withDensity_iff_ae_restrict' {p : α → Prop} {f : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) :
    (∀ᵐ x ∂μ.withDensity f, p x) ↔ ∀ᵐ x ∂μ.restrict { x | f x ≠ 0 }, p x

Proof state:
α : 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
⊢ {x | g x ≠ 0} a

Tactic:
rwa [ha] at h

Result:
no goals

Proof state:
α : 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
⊢ {x | f x ≠ 0} a

Tactic:
rwa [← ha] at h

Result:
no goals

Proof state:
α : 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:
filter_upwards [hfg] with a ha

Result:
case h
α : 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

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ NullMeasurableSet {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⟩

Result:
case intro.intro
α : 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} μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → p x

Tactic:
simp only [mem_setOf]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ NullMeasurableSet {x | f x ≠ 0} μ

Tactic:
rcases hf with ⟨g, hg, hfg⟩

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ NullMeasurableSet {x | f x ≠ 0} μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, p x

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

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → p x

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ NullMeasurableSet {x | f x ≠ 0} μ

Proof state:
case intro.intro
α : 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

Result:
no goals

Proof state:
case h
α : 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⟩

Result:
no goals

Proof state:
case h
α : 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:
simp only [eq_iff_iff]

Result:
case h
α : 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