-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_average_norm_sub {f : α → E} (hf : LocallyIntegrable f μ) :
    ∀ᵐ x ∂μ, Tendsto (fun a => ⨍ y in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ⊤
h''a : IntegrableOn f a μ
⊢ IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ

Tactic:
simp_rw [coe_nnnorm]

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ⊤
h''a : IntegrableOn f a μ
⊢ IntegrableOn (fun y => ‖f y - f x‖) a μ

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Tactic:
have := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hx

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 (ENNReal.toReal 0))
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ⊤
h''a : IntegrableOn f a μ
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ
⊢ (μ a).toReal⁻¹ * (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ).toReal = (μ a).toReal⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal (by positivity)]

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ⊤
h''a : IntegrableOn f a μ
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ
⊢ (μ a).toReal⁻¹ * ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ = (μ a).toReal⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ⊤
h''a : IntegrableOn f a μ
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ
⊢ 0 ≤ ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 (ENNReal.toReal 0))
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Tactic:
simp only [ENNReal.zero_toReal] at this

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Tactic:
apply Tendsto.congr' _ this

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) =ᶠ[v.filterAt x] fun a =>
    ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
a : Set α
h'a : μ a < ⊤
h''a : IntegrableOn f a μ
A : IntegrableOn (fun y => ↑‖f y - f x‖₊) a μ
⊢ (μ a).toReal⁻¹ * ∫ (a : α) in a, ↑‖f a - f x‖₊ ∂μ = (μ a).toReal⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
simp only [coe_nnnorm, smul_eq_mul]

Result:
no goals