-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean
theorem aestronglyMeasurable_withDensity_iff {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] {f : α → ℝ≥0} (hf : Measurable f) {g : α → E} :
    AEStronglyMeasurable g (μ.withDensity fun x => (f x : ℝ≥0∞)) ↔
      AEStronglyMeasurable (fun x => (f x : ℝ) • g x) μ

Proof state:
case mp.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ

Tactic:
have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl

Result:
case mp.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ

Tactic:
constructor

Result:
case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x => ↑(f x)) → AEStronglyMeasurable (fun x => ↑(f x) • g x) μ

case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ → AEStronglyMeasurable g (μ.withDensity fun x => ↑(f x))

Proof state:
case mpr.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] fun x => (↑(f x))⁻¹ • g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]

Result:
case mpr.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x

Proof state:
case mp.intro.intro.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x

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

Result:
case mp.intro.intro.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : x ∈ {x | f x ≠ 0}ᶜ
⊢ ↑(f x) • g x = ↑(f x) • g' x

Tactic:
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : f x = 0
⊢ ↑(f x) • g x = ↑(f x) • g' x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h'a

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : f x = 0
⊢ ↑(f x) • g x = ↑(f x) • g' x

Tactic:
simp [hx]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x

Tactic:
rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0

Proof state:
case mp.intro.intro.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x

Tactic:
rw [ae_restrict_iff' A]

Result:
case mp.intro.intro.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa only [NNReal.coe_eq_zero, Ne] using h'x

Result:
no goals

Proof state:
case mp.intro.intro.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x

Tactic:
filter_upwards [hg'] with a ha h'a

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a