-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_lintegral_enorm_sub_div'_of_integrable {f : α → E} (hf : Integrable f μ)
    (h'f : StronglyMeasurable f) :
    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
    (𝓝 ‖f x - c‖ₑ)
a : Set α
ha : a ⊆ A.set n
h'a : MeasurableSet a
⊢ (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a = (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a

Tactic:
congr 1

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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
    (𝓝 ‖f x - c‖ₑ)
a : Set α
ha : a ⊆ A.set n
h'a : MeasurableSet a
⊢ ∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ

Proof state:
case intro.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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
filter_upwards [main, v.ae_eventually_measure_pos] with x hx h'x

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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
rcases h'f.isSeparable_range with ⟨t, t_count, ht⟩

Result:
case intro.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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
n : ℕ
c : E
hi✝ : c ∈ t
⊢ Integrable ((A.set n).indicator fun x => c) μ

Tactic:
simp only [integrable_indicator_iff (IsOpen.measurableSet (A.set_mem n)),
  integrableOn_const, A.finite n, or_true]

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 : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
    (𝓝 ‖f x - c‖ₑ)
a : Set α
ha : a ⊆ A.set n
h'a : MeasurableSet a
y : α
hy : y ∈ a
⊢ ‖f y - (A.set n).indicator (fun x => c) y‖ₑ = ‖f y - c‖ₑ

Tactic:
simp only [ha hy, indicator_of_mem]

Result:
no goals