-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_lintegral_div {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (h'f : (∫⁻ y, f y ∂μ) ≠ ∞) :
    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Proof state:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))

Tactic:
convert hx using 1

Result:
case h.e'_3
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) = fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤

Tactic:
convert h'f using 1

Result:
case h.e'_2
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ = ∫⁻ (y : α), f y ∂μ

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Tactic:
filter_upwards [v.ae_tendsto_lintegral_div' hf.measurable_mk A, hf.ae_eq_mk] with x hx h'x

Result:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Tactic:
have A : (∫⁻ y, hf.mk f y ∂μ) ≠ ∞ := by
  convert h'f using 1
  apply lintegral_congr_ae
  exact hf.ae_eq_mk.symm

Result:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))

Proof state:
case h.e'_2
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ = ∫⁻ (y : α), f y ∂μ

Tactic:
apply lintegral_congr_ae

Result:
case h.e'_2.h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
⊢ AEMeasurable.mk f hf =ᶠ[ae μ] f

Proof state:
case h.e'_2.h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
⊢ AEMeasurable.mk f hf =ᶠ[ae μ] f

Tactic:
exact hf.ae_eq_mk.symm

Result:
no goals

Proof state:
case h.e'_3.h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ (∫⁻ (y : α) in a, f y ∂μ) / μ a = (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a

Tactic:
congr 1

Result:
case h.e'_3.h.e_a
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ ∫⁻ (y : α) in a, f y ∂μ = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ

Proof state:
case h.e'_3.h.e_a.h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤
x : α
hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ f =ᶠ[ae (μ.restrict a)] AEMeasurable.mk f hf

Tactic:
exact ae_restrict_of_ae hf.ae_eq_mk

Result:
no goals