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

Proof state:
case hf
α : 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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
n : ℕ
⊢ Integrable ((u n).indicator f) μ

Tactic:
exact (integrable_indicator_iff (u_open n).measurableSet).2 (hu n)

Result:
no goals

Proof state:
case h.intro
α : 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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
apply Tendsto.congr' _ (hx n)

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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
⊢ (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) =ᶠ[v.filterAt x] fun a =>
    (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a

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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ ∃ n, x ∈ u n

Tactic:
simpa only [← u_univ, mem_iUnion] using mem_univ x

Result:
no goals

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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
apply ae_tendsto_lintegral_enorm_sub_div_of_integrable

Result:
case hf
α : 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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
n : ℕ
⊢ Integrable ((u n).indicator f) μ

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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
obtain ⟨n, hn⟩ : ∃ n, x ∈ u n := by simpa only [← u_univ, mem_iUnion] using mem_univ x

Result:
case h.intro
α : 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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Proof state:
case h.e_a
α : 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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
a : Set α
ha : a ⊆ u n
h'a : MeasurableSet a
⊢ ∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ

Tactic:
refine setLIntegral_congr_fun h'a (Eventually.of_forall (fun y hy ↦ ?_))

Result:
case h.e_a
α : 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 μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
a : Set α
ha : a ⊆ u n
h'a : MeasurableSet a
y : α
hy : y ∈ a
⊢ ‖(u n).indicator f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ